src/Pure/Isar/proof.ML
changeset 6853 80f88b762816
parent 6848 3d82756e1af5
child 6871 01866edde713
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 28 23:02:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Jun 28 23:02:38 1999 +0200
     1.3 @@ -398,16 +398,13 @@
     1.4  
     1.5  (* solve goal *)
     1.6  
     1.7 -fun REV_RANGE _ [] = all_tac
     1.8 -  | REV_RANGE k (tac :: tacs) = tac k THEN REV_RANGE (k - 1) tacs;
     1.9 +fun RANGE [] _ = all_tac
    1.10 +  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
    1.11  
    1.12  fun solve_goal rule tacs state =
    1.13    let
    1.14 -    val rev_tacs = rev tacs;
    1.15 -    val n = length rev_tacs - 1;
    1.16 -
    1.17      val (_, (result, (facts, thm))) = find_goal 0 state;
    1.18 -    val thms' = FIRSTGOAL (rtac rule THEN' (fn i => REV_RANGE (i + n) rev_tacs)) thm;
    1.19 +    val thms' = FIRSTGOAL (rtac rule THEN' RANGE tacs) thm;
    1.20    in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
    1.21  
    1.22