--- a/src/Provers/order.ML Wed May 07 10:59:48 2008 +0200
+++ b/src/Provers/order.ML Wed May 07 10:59:49 2008 +0200
@@ -411,10 +411,13 @@
where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
other relation symbols cause an error message *)
-fun gen_order_tac mkasm mkconcl decomp (less_thms : less_arith) prems =
+fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) prems =
let
+fun decomp sign t = Option.map (fn (x, rel, y) =>
+ (Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t);
+
(* ******************************************************************* *)
(* *)
(* mergeLess *)