asm_full_simp_tac now fails when applied to a state w/o subgoals.

--- 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);