# HG changeset patch
# User berghofe
# Date 1210150789 -7200
# Node ID 87a5b9ec3863467c2d171854044688c6d42bfcb2
# Parent  7c3757fccf0e4848952b72cfbf6b47d89f6668c3
Terms returned by decomp are now eta-contracted.

diff -r 7c3757fccf0e -r 87a5b9ec3863 src/Provers/order.ML
--- 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                                                           *)
diff -r 7c3757fccf0e -r 87a5b9ec3863 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Wed May 07 10:59:48 2008 +0200
+++ b/src/Provers/trancl.ML	Wed May 07 10:59:49 2008 +0200
@@ -87,10 +87,14 @@
 
 exception Cannot; (* internal exception: raised if no proof can be found *)
 
+fun decomp t = Option.map (fn (x, y, rel, r) =>
+  (Envir.beta_eta_contract x, Envir.beta_eta_contract y,
+   Envir.beta_eta_contract rel, r)) (Cls.decomp t);
+
 fun prove thy r asms = 
   let
     fun inst thm =
-      let val SOME (_, _, r', _) = Cls.decomp (concl_of thm)
+      let val SOME (_, _, r', _) = decomp (concl_of thm)
       in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
     fun pr (Asm i) = List.nth (asms, i)
       | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
@@ -124,7 +128,7 @@
 (* ************************************************************************ *)
 
 fun mkasm_trancl  Rel  (t, n) =
-  case Cls.decomp t of
+  case decomp t of
     SOME (x, y, rel,r) => if rel aconv Rel then  
     
     (case r of
@@ -147,7 +151,7 @@
 (* ************************************************************************ *)
 
 fun mkasm_rtrancl Rel (t, n) =
-  case Cls.decomp t of
+  case decomp t of
    SOME (x, y, rel, r) => if rel aconv Rel then
     (case r of
       "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
@@ -171,14 +175,14 @@
 (* ************************************************************************ *)
 
 fun mkconcl_trancl  t =
-  case Cls.decomp t of
+  case decomp t of
     SOME (x, y, rel, r) => (case r of
       "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
     | _     => raise Cannot)
   | NONE => raise Cannot;
 
 fun mkconcl_rtrancl  t =
-  case Cls.decomp t of
+  case decomp t of
     SOME (x,  y, rel,r ) => (case r of
       "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
     | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)