--- 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