changeset 26653 | 60e0cf6bef89 |
parent 26497 | 1873915c64a9 |
child 27021 | 4593b9f4ba42 |
--- a/src/Pure/simplifier.ML Tue Apr 15 16:12:01 2008 +0200 +++ b/src/Pure/simplifier.ML Tue Apr 15 16:12:05 2008 +0200 @@ -417,7 +417,7 @@ if can Logic.dest_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 mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm); in empty_ss setsubgoaler asm_simp_tac setSSolver safe_solver