--- a/src/HOL/simpdata.ML Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/simpdata.ML Tue Sep 21 19:11:07 1999 +0200
@@ -429,14 +429,18 @@
fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
-fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems),
- atac , etac FalseE ];
+fun unsafe_solver_tac prems =
+ FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
+val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
+
(*No premature instantiation of variables during simplification*)
-fun safe_solver prems = FIRST'[ match_tac(reflexive_thm::TrueI::refl::prems),
- eq_assume_tac, ematch_tac [FalseE]];
+fun safe_solver_tac prems =
+ FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
+ eq_assume_tac, ematch_tac [FalseE]];
+val safe_solver = mk_solver "HOL safe" safe_solver_tac;
val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
- setSSolver safe_solver
+ setSSolver safe_solver
setSolver unsafe_solver
setmksimps (mksimps mksimps_pairs)
setmkeqTrue mk_eq_True;