# HG changeset patch
# User wenzelm
# Date 1237293201 -3600
# Node ID a28d83e903ce8f1c107151f9917cb7807e80e8ca
# Parent  7be15917f3faa6f582faea6a4e527b89ff68dfb8
goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;

diff -r 7be15917f3fa -r a28d83e903ce src/Pure/Isar/proof.ML
--- 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