# HG changeset patch
# User wenzelm
# Date 950557392 -3600
# Node ID 5db67376df7d8d7006257deaee8826d69336c0bc
# Parent  ac8ac0eba73836523a3eecf4c6020cf4b0f5471b
easy_setup: fixed mksimps;

diff -r ac8ac0eba738 -r 5db67376df7d src/Provers/simplifier.ML
--- 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