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