src/Pure/more_thm.ML

--- a/src/Pure/more_thm.ML	Fri Oct 15 17:45:47 2021 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 15 19:25:31 2021 +0200
@@ -336,36 +336,48 @@
 
 local
 
-fun dest_all ct =
+val used_frees =
+  Name.build_context o
+    Thm.fold_terms {hyps = true} Term.declare_term_frees;
+
+fun used_vars i =
+  Name.build_context o
+    (Thm.fold_terms {hyps = false} o Term.fold_aterms)
+      (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I);
+
+fun dest_all ct used =
   (case Thm.term_of ct of
-    Const ("Pure.all", _) $ Abs (a, _, _) =>
-      let val (x, ct') = Thm.dest_abs (Thm.dest_arg ct)
-      in SOME ((a, Thm.ctyp_of_cterm x), ct') end
+    Const ("Pure.all", _) $ Abs (x, _, _) =>
+      let
+        val (x', used') = Name.variant x used;
+        val (v, ct') = Thm.dest_abs_fresh x' (Thm.dest_arg ct);
+      in SOME ((x, Thm.ctyp_of_cterm v), (ct', used')) end
   | _ => NONE);
 
-fun dest_all_list ct =
-  (case dest_all ct of
-    NONE => []
-  | SOME (v, ct') => v :: dest_all_list ct');
+fun dest_all_list ct used =
+  (case dest_all ct used of
+    NONE => ([], used)
+  | SOME (v, (ct', used')) =>
+      let val (vs, used'') = dest_all_list ct' used'
+      in (v :: vs, used'') end);
 
 fun forall_elim_vars_list vars i th =
   let
-    val used =
-      (Thm.fold_terms {hyps = false} o Term.fold_aterms)
-        (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
-    val vars' = (Name.variant_list used (map #1 vars), vars)
-      |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
+    val (vars', _) =
+      (vars, used_vars i th) |-> fold_map (fn (x, T) => fn used =>
+        let val (x', used') = Name.variant x used
+        in (Thm.var ((x', i), T), used') end);
   in fold Thm.forall_elim vars' th end;
 
 in
 
 fun forall_elim_vars i th =
-  forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th;
+  forall_elim_vars_list (#1 (dest_all_list (Thm.cprop_of th) (used_frees th))) i th;
 
 fun forall_elim_var i th =
   let
     val vars =
-      (case dest_all (Thm.cprop_of th) of
+      (case dest_all (Thm.cprop_of th) (used_frees th) of
         SOME (v, _) => [v]
       | NONE => raise THM ("forall_elim_var", i, [th]));
   in forall_elim_vars_list vars i th end;