# HG changeset patch
# User wenzelm
# Date 1237313164 -3600
# Node ID cd8e20f86795407690a71c1c81224605827d7b8f
# Parent  9643f54c41843b5ff2a4c5411c8807320c1430e2
close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;

diff -r 9643f54c4184 -r cd8e20f86795 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Mar 17 16:55:21 2009 +0100
+++ b/src/Pure/Isar/method.ML	Tue Mar 17 19:06:04 2009 +0100
@@ -39,6 +39,7 @@
   val this: method
   val fact: thm list -> Proof.context -> method
   val assm_tac: Proof.context -> int -> tactic
+  val all_assm_tac: Proof.context -> tactic
   val assumption: Proof.context -> method
   val close: bool -> Proof.context -> method
   val trace: Proof.context -> thm list -> unit
@@ -223,14 +224,15 @@
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;
 
+fun all_assm_tac ctxt st = EVERY1 (replicate (Thm.nprems_of st) (assm_tac ctxt)) st;
+
 fun assumption ctxt = METHOD (HEADGOAL o
   (fn [] => assm_tac ctxt
     | [fact] => solve_tac [fact]
     | _ => K no_tac));
 
 fun close immed ctxt = METHOD (K
-  (FILTER Thm.no_prems
-    ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
+  (FILTER Thm.no_prems ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac)));
 
 end;