# HG changeset patch
# User ballarin
# Date 1190906885 -7200
# Node ID a53f5db5acbb040d71aec6c8460af43b5cea3f3d
# Parent  36750aca7a77c35bd45b888af8d7f0626fcac594
Fixed setup of transitivity reasoner (function decomp).

diff -r 36750aca7a77 -r a53f5db5acbb src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Sep 27 17:22:15 2007 +0200
+++ b/src/HOL/Orderings.thy	Thu Sep 27 17:28:05 2007 +0200
@@ -293,16 +293,17 @@
           in
 	    T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
           end;
-	fun dec (Const (@{const_name Not}, _) $ t) = (case dec t
-	      of NONE => NONE
-	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
-          | dec (bin_op $ t1 $ t2) =
+	fun rel (bin_op $ t1 $ t2) =
               if excluded t1 then NONE
               else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
               else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
               else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
               else NONE
-	  | dec _ = NONE;
+	  | rel _ = NONE;
+	fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
+	      of NONE => NONE
+	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
+          | dec x = rel x;
       in dec t end;
   in
     case s of