# HG changeset patch
# User wenzelm
# Date 1010757185 -3600
# Node ID 41e0d086f8b6b65892002a2d88d507b6b458766c
# Parent  ade42a6c22ad85ea46bdc80bf1d1e3ed597fa1a1
improved forall_elim_vars_safe (no longer invents new indexes);

diff -r ade42a6c22ad -r 41e0d086f8b6 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jan 11 14:44:58 2002 +0100
+++ b/src/Pure/drule.ML	Fri Jan 11 14:53:05 2002 +0100
@@ -315,10 +315,12 @@
 val forall_elim_var = PureThy.forall_elim_var;
 val forall_elim_vars = PureThy.forall_elim_vars;
 
-fun forall_elim_vars_safe th =
-  forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th)
-    handle THM _ => th;
-
+fun forall_elim_vars_safe thm =
+  let
+    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
+    fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
+    val vs = Term.strip_all_vars prop;
+  in foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
 
 (*Specialization over a list of cterms*)
 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);