# HG changeset patch
# User wenzelm
# Date 930603758 -7200
# Node ID 80f88b762816584e2a8fb108909857485e6579df
# Parent  fe39a3054d8222179ef6e4c032b62e6b455bd2f3
improved RANGE;

diff -r fe39a3054d82 -r 80f88b762816 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jun 28 23:02:03 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jun 28 23:02:38 1999 +0200
@@ -398,16 +398,13 @@
 
 (* solve goal *)
 
-fun REV_RANGE _ [] = all_tac
-  | REV_RANGE k (tac :: tacs) = tac k THEN REV_RANGE (k - 1) tacs;
+fun RANGE [] _ = all_tac
+  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
 
 fun solve_goal rule tacs state =
   let
-    val rev_tacs = rev tacs;
-    val n = length rev_tacs - 1;
-
     val (_, (result, (facts, thm))) = find_goal 0 state;
-    val thms' = FIRSTGOAL (rtac rule THEN' (fn i => REV_RANGE (i + n) rev_tacs)) thm;
+    val thms' = FIRSTGOAL (rtac rule THEN' RANGE tacs) thm;
   in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;