asm_full_simp_tac now fails if there are no subgoals
authornipkow
Thu, 25 Nov 1993 13:41:08 +0100
changeset 146 dbee71d43339
parent 145 422197c5a078
child 147 e8d8fa0ddcef
asm_full_simp_tac now fails if there are no subgoals
src/Provers/simplifier.ML
--- 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);