author | nipkow |
Thu, 25 Nov 1993 13:41:08 +0100 | |
changeset 146 | dbee71d43339 |
parent 145 | 422197c5a078 |
child 147 | e8d8fa0ddcef |
--- a/src/Provers/simplifier.ML Thu Nov 25 11:49:21 1993 +0100 +++ b/src/Provers/simplifier.ML Thu Nov 25 13:41:08 1993 +0100 @@ -156,7 +156,7 @@ and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) and simp_loop_tac i = Tactic(simp_loop i) - in fn i => COND (has_fewer_prems 0) no_tac (simp_loop_tac i) end; + in fn i => COND (has_fewer_prems 1) no_tac (simp_loop_tac i) end; fun asm_simp_tac ss = METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);