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