fix adaptation note

Plausible/Gen.lean

@@ -98,21 +98,14 @@ def elements (xs : List α) (pos : 0 < xs.length) : Gen α := do
   return xs[x]
 
 
-/-!
-adaptation_note
-
-Due to an error in `nightly-2025-01-04`, we temporarily need `open Classical in` here,
-and `(α := α)` at the call site of `List.perm_insertIdx`. Both should be removed after `nightly-2025-01-05` is available.
--/
 open List in
-open Classical in
 /-- Generate a random permutation of a given list. -/
 def permutationOf : (xs : List α) → Gen { ys // xs ~ ys }
   | [] => pure ⟨[], Perm.nil⟩
   | x::xs => do
     let ⟨ys, h1⟩ ← permutationOf xs
     let ⟨n, _, h3⟩ ← up <| choose Nat 0 ys.length (by omega)
-    return ⟨insertIdx n x ys, Perm.trans (Perm.cons _ h1) (List.perm_insertIdx (α := α) _ _ h3).symm⟩
+    return ⟨insertIdx n x ys, Perm.trans (Perm.cons _ h1) (List.perm_insertIdx _ _ h3).symm⟩
 
 /-- Given two generators produces a tuple consisting out of the result of both -/
 def prodOf {α : Type u} {β : Type v} (x : Gen α) (y : Gen β) : Gen (α × β) := do

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-01-04
+leanprover/lean4:nightly-2025-01-05