diff -r 98cb63b447c6 -r 44c0028486db src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Sat Nov 30 16:42:22 2024 +0100
+++ b/src/Tools/IsaPlanner/isand.ML	Sat Nov 30 17:14:30 2024 +0100
@@ -56,10 +56,7 @@
   let
     val names =
       Variable.names_of ctxt
-      |> (fold o fold_aterms)
-          (fn Var ((a, _), _) => Name.declare a
-            | Free (a, _) => Name.declare a
-            | _ => I) ts;
+      |> fold (fn t => Term.declare_free_names t #> Term.declare_var_names (K true) t) ts;
   in fst (fold_map Name.variant xs names) end;
 
 (* fix parameters of a subgoal "i", as free variables, and create an