changeset 146 | dbee71d43339 |
parent 88 | 9df4dfedee01 |
child 217 | c972c57e7762 |
--- 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);