src/FOL/simpdata.ML
changeset 12720 f8a134b9a57f
parent 12526 1b9db2581fe2
child 12725 7ede865e1fe5
--- 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 ***)