diff -r 37c0b5a7ee5d -r b85c77b64c7a src/FOL/ex/mini.ML
--- a/src/FOL/ex/mini.ML	Sat Feb 15 17:43:27 1997 +0100
+++ b/src/FOL/ex/mini.ML	Sat Feb 15 17:44:10 1997 +0100
@@ -60,14 +60,7 @@
                  "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
 
 
-val mini_ss = 
-  empty_ss 
-  setmksimps (map mk_meta_eq o atomize o gen_all)
-  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
-                          ORELSE' assume_tac
-                          ORELSE' etac FalseE)
-  setsubgoaler asm_simp_tac
-  addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
+val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
 
 val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss;