| changeset 6104 | 55c7f8f0bb4d |
| parent 6091 | e3cdbd929a24 |
| child 6108 | 2c9ed58c30ba |
--- 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 *)