avoid upto if not needed
authorhaftmann
Mon Oct 26 15:16:28 2009 +0100 (2009-10-26)
changeset 33206fee21bb23d22
parent 33205 20587741a8d9
child 33207 e6c3e05181f1
avoid upto if not needed
src/Provers/order.ML
src/Pure/library.ML
     1.1 --- a/src/Provers/order.ML	Mon Oct 26 15:15:59 2009 +0100
     1.2 +++ b/src/Provers/order.ML	Mon Oct 26 15:16:28 2009 +0100
     1.3 @@ -307,7 +307,7 @@
     1.4  (*                                                                          *)
     1.5  (* ************************************************************************ *)
     1.6  
     1.7 -fun mkasm_partial decomp (less_thms : less_arith) sign (t, n) =
     1.8 +fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) =
     1.9    case decomp sign t of
    1.10      SOME (x, rel, y) => (case rel of
    1.11        "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
    1.12 @@ -335,7 +335,7 @@
    1.13  (*                                                                          *)
    1.14  (* ************************************************************************ *)
    1.15  
    1.16 -fun mkasm_linear decomp (less_thms : less_arith) sign (t, n) =
    1.17 +fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) =
    1.18    case decomp sign t of
    1.19      SOME (x, rel, y) => (case rel of
    1.20        "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
    1.21 @@ -1228,7 +1228,7 @@
    1.22     val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
    1.23     val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    1.24     val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
    1.25 -   val lesss = flat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
    1.26 +   val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
    1.27     val prfs = gen_solve mkconcl thy (lesss, C);
    1.28     val (subgoals, prf) = mkconcl decomp less_thms thy C;
    1.29    in
     2.1 --- a/src/Pure/library.ML	Mon Oct 26 15:15:59 2009 +0100
     2.2 +++ b/src/Pure/library.ML	Mon Oct 26 15:16:28 2009 +0100
     2.3 @@ -853,7 +853,7 @@
     2.4       of [] => 0
     2.5        | [n] => n
     2.6        | _ => raise UnequalLengths;
     2.7 -  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
     2.8 +  in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
     2.9  
    2.10  
    2.11