# HG changeset patch
# User nipkow
# Date 749478382 -3600
# Node ID b35851cafd3e323b6dfd6861a15db6320f21cb46
# Parent  0b033d50ca1c70826f15871feec3fbb7e9acea86
asm_full_simp_tac now fails when applied to a state w/o subgoals.

diff -r 0b033d50ca1c -r b35851cafd3e src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Sep 30 10:54:01 1993 +0100
+++ b/src/Provers/simplifier.ML	Fri Oct 01 13:26:22 1993 +0100
@@ -146,7 +146,7 @@
       and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
       and simp_loop_tac i = Tactic(simp_loop i)
 
-  in simp_loop_tac end;
+  in fn i => COND (has_fewer_prems 0) no_tac (simp_loop_tac i) end;
 
 fun asm_simp_tac ss =
       METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);