--- 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 =