# 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;