Fixed setup of transitivity reasoner (function decomp).

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