diff -r beedc794bd67 -r 7ede865e1fe5 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Sequents/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
@@ -240,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 forall_elim_vars_safe)
+    setmksimps (map mk_meta_eq o atomize o gen_all)
     setmkcong mk_meta_cong;
 
 val LK_simps =