improved forall_elim_vars_safe (no longer invents new indexes);

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