goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;

--- a/src/Pure/Isar/proof.ML	Tue Mar 17 12:10:42 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Mar 17 13:33:21 2009 +0100
@@ -440,12 +440,18 @@
 
 (* refine via sub-proof *)
 
+fun finish_tac 0 = K all_tac
+  | finish_tac n =
+      Goal.norm_hhf_tac THEN'
+      SUBGOAL (fn (goal, i) =>
+        if can Logic.unprotect (Logic.strip_assums_concl goal) then
+          Tactic.etac Drule.protectI i THEN finish_tac (n - 1) i
+        else finish_tac (n - 1) (i + 1));
+
 fun goal_tac rule =
-  Goal.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
-    (Goal.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
-      if can Logic.unprotect (Logic.strip_assums_concl goal) then
-        Tactic.etac Drule.protectI i
-      else all_tac)));
+  Goal.norm_hhf_tac THEN'
+  Tactic.rtac rule THEN'
+  finish_tac (Thm.nprems_of rule);
 
 fun refine_goals print_rule inner raw_rules state =
   let