1.1 --- a/src/HOL/Orderings.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -339,18 +339,18 @@
     1.4            (* exclude numeric types: linear arithmetic subsumes transitivity *)
     1.5            let val T = type_of t
     1.6            in
     1.7 -	    T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
     1.8 +            T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
     1.9            end;
    1.10 -	fun rel (bin_op $ t1 $ t2) =
    1.11 +        fun rel (bin_op $ t1 $ t2) =
    1.12                if excluded t1 then NONE
    1.13                else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
    1.14                else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
    1.15                else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
    1.16                else NONE
    1.17 -	  | rel _ = NONE;
    1.18 -	fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
    1.19 -	      of NONE => NONE
    1.20 -	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
    1.21 +          | rel _ = NONE;
    1.22 +        fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
    1.23 +              of NONE => NONE
    1.24 +               | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
    1.25            | dec x = rel x;
    1.26        in dec t end
    1.27        | decomp thy _ = NONE;