# HG changeset patch
# User nipkow
# Date 754231268 -3600
# Node ID dbee71d43339b4fbffc841f426ae525543753e20
# Parent  422197c5a0780171fc87efcc2227ecb78b8aaa0e
asm_full_simp_tac now fails if there are no subgoals

diff -r 422197c5a078 -r dbee71d43339 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);