--- a/src/Provers/simplifier.ML Mon Feb 14 20:42:02 2000 +0100
+++ b/src/Provers/simplifier.ML Mon Feb 14 20:43:12 2000 +0100
@@ -526,10 +526,12 @@
fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
val safe_solver = mk_solver "easy safe" safe_solver_tac;
- fun mksimps thm =
+ fun mk_eq thm =
if Logic.is_equals (Thm.concl_of thm) then [thm]
else [thm RS reflect] handle THM _ => [];
+ fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
+
fun init_ss thy =
(simpset_ref_of thy :=
empty_ss setsubgoaler asm_simp_tac