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