# HG changeset patch
# User berghofe
# Date 1037198115 -3600
# Node ID 34ef15959ce731dee6a16f2d5dcda3f991a03532
# Parent  82d7fc25a2250df516a040f9ca5a85cde95e7ac5
Fixed name clash problem in forall_elim_var.

diff -r 82d7fc25a225 -r 34ef15959ce7 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Nov 13 15:34:35 2002 +0100
+++ b/src/Pure/pure_thy.ML	Wed Nov 13 15:35:15 2002 +0100
@@ -378,14 +378,15 @@
 
 (* forall_elim_vars (belongs to drule.ML) *)
 
-(*Replace outermost quantified variable by Var of given index.
-    Could clash with Vars already present.*)
+(*Replace outermost quantified variable by Var of given index.*)
 fun forall_elim_var i th =
     let val {prop,sign,...} = rep_thm th
     in case prop of
-          Const("all",_) $ Abs(a,T,_) =>
-              forall_elim (cterm_of sign (Var((a,i), T)))  th
-        | _ => raise THM("forall_elim_var", i, [th])
+        Const ("all", _) $ Abs (a, T, _) =>
+          let val used = map (fst o fst)
+            (filter (equal i o snd o fst) (Term.add_vars ([], prop)))
+          in forall_elim (cterm_of sign (Var ((variant used a, i), T))) th end
+      | _ => raise THM ("forall_elim_var", i, [th])
     end;
 
 (*Repeat forall_elim_var until all outer quantifiers are removed*)