# HG changeset patch
# User wenzelm
# Date 916155871 -3600
# Node ID 55c7f8f0bb4d9447878d22df1aea27880b4b9557
# Parent  36f272ea94131fd656f0f164ca2283defd6fbc68
improved asm_finish;

diff -r 36f272ea9413 -r 55c7f8f0bb4d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jan 12 16:42:21 1999 +0100
+++ b/src/Pure/Isar/method.ML	Tue Jan 12 16:44:31 1999 +0100
@@ -92,7 +92,7 @@
 val trivial = METHOD (ALLGOALS o trivial_tac);
 val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
 
-val asm_finish = METHOD (K (TRYALL assume_tac));
+val asm_finish = METHOD (K (FILTER (equal 0 o Thm.nprems_of) (ALLGOALS assume_tac)));
 
 
 (* rule *)