# HG changeset patch
# User haftmann
# Date 1256566588 -3600
# Node ID fee21bb23d22e731d3e9e3ca5c2b4e51798062bb
# Parent  20587741a8d9a12808fde4382ca3a9155c1e9d81
avoid upto if not needed

diff -r 20587741a8d9 -r fee21bb23d22 src/Provers/order.ML
--- a/src/Provers/order.ML	Mon Oct 26 15:15:59 2009 +0100
+++ b/src/Provers/order.ML	Mon Oct 26 15:16:28 2009 +0100
@@ -307,7 +307,7 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkasm_partial decomp (less_thms : less_arith) sign (t, n) =
+fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) =
   case decomp sign t of
     SOME (x, rel, y) => (case rel of
       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
@@ -335,7 +335,7 @@
 (*                                                                          *)
 (* ************************************************************************ *)
 
-fun mkasm_linear decomp (less_thms : less_arith) sign (t, n) =
+fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) =
   case decomp sign t of
     SOME (x, rel, y) => (case rel of
       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
@@ -1228,7 +1228,7 @@
    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
    val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-   val lesss = flat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
+   val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
    val prfs = gen_solve mkconcl thy (lesss, C);
    val (subgoals, prf) = mkconcl decomp less_thms thy C;
   in
diff -r 20587741a8d9 -r fee21bb23d22 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Oct 26 15:15:59 2009 +0100
+++ b/src/Pure/library.ML	Mon Oct 26 15:16:28 2009 +0100
@@ -853,7 +853,7 @@
      of [] => 0
       | [n] => n
       | _ => raise UnequalLengths;
-  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
+  in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;