# HG changeset patch
# User wenzelm
# Date 1010757210 -3600
# Node ID f8a134b9a57fa68aaec3e5f978ea37e56ce44e8a
# Parent  41e0d086f8b6b65892002a2d88d507b6b458766c
replace gen_all by forall_elim_vars_safe;

diff -r 41e0d086f8b6 -r f8a134b9a57f src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Jan 11 14:53:05 2002 +0100
+++ b/src/FOL/simpdata.ML	Fri Jan 11 14:53:30 2002 +0100
@@ -68,8 +68,6 @@
 
 (** Conversion into rewrite rules **)
 
-fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-
 bind_thm ("P_iff_F", int_prove_fun "~P ==> (P <-> False)");
 bind_thm ("iff_reflection_F", P_iff_F RS iff_reflection);
 
@@ -123,7 +121,7 @@
          | _ => [th])
   in atoms end;
 
-fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
+fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
 
 (*** Classical laws ***)
 
diff -r 41e0d086f8b6 -r f8a134b9a57f src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri Jan 11 14:53:05 2002 +0100
+++ b/src/Sequents/simpdata.ML	Fri Jan 11 14:53:30 2002 +0100
@@ -83,9 +83,6 @@
 
 (** Conversion into rewrite rules **)
 
-fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-
-
 (*Make atomic rewrite rules*)
 fun atomize r =
  case concl_of r of
@@ -243,7 +240,7 @@
   empty_ss setsubgoaler asm_simp_tac
     setSSolver (mk_solver "safe" safe_solver)
     setSolver (mk_solver "unsafe" unsafe_solver)
-    setmksimps (map mk_meta_eq o atomize o gen_all)
+    setmksimps (map mk_meta_eq o atomize o forall_elim_vars_safe)
     setmkcong mk_meta_cong;
 
 val LK_simps =
diff -r 41e0d086f8b6 -r f8a134b9a57f src/ZF/Main.ML
--- a/src/ZF/Main.ML	Fri Jan 11 14:53:05 2002 +0100
+++ b/src/ZF/Main.ML	Fri Jan 11 14:53:30 2002 +0100
@@ -4,4 +4,4 @@
   val thy = the_context ();
 end;
 
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe);
diff -r 41e0d086f8b6 -r f8a134b9a57f src/ZF/OrdQuant.ML
--- a/src/ZF/OrdQuant.ML	Fri Jan 11 14:53:05 2002 +0100
+++ b/src/ZF/OrdQuant.ML	Fri Jan 11 14:53:30 2002 +0100
@@ -103,7 +103,7 @@
 
 val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe)
                         addsimps [oall_simp, ltD RS beta]
                         addcongs [oall_cong, oex_cong, OUN_cong];
 
diff -r 41e0d086f8b6 -r f8a134b9a57f src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Jan 11 14:53:05 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 11 14:53:30 2002 +0100
@@ -341,7 +341,7 @@
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
      val min_ss = empty_ss
-           setmksimps (map mk_eq o ZF_atomize o gen_all)
+           setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
            setSolver (mk_solver "minimal"
                       (fn prems => resolve_tac (triv_rls@prems)
                                    ORELSE' assume_tac
diff -r 41e0d086f8b6 -r f8a134b9a57f src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Fri Jan 11 14:53:05 2002 +0100
+++ b/src/ZF/simpdata.ML	Fri Jan 11 14:53:30 2002 +0100
@@ -46,7 +46,7 @@
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
 simpset_ref() :=
-  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
+  simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
   addcongs [if_weak_cong]
   addsplits [split_if]
   setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));