src/HOL/Orderings.thy
changeset 30107 f3b3b0e3d184
parent 29823 0ab754d13ccd
child 30298 abefe1dfadbb
     1.1 --- a/src/HOL/Orderings.thy	Wed Feb 25 11:30:46 2009 -0800
     1.2 +++ b/src/HOL/Orderings.thy	Thu Feb 26 16:32:46 2009 +0100
     1.3 @@ -331,7 +331,7 @@
     1.4  
     1.5  fun struct_tac ((s, [eq, le, less]), thms) prems =
     1.6    let
     1.7 -    fun decomp thy (Trueprop $ t) =
     1.8 +    fun decomp thy (@{const Trueprop} $ t) =
     1.9        let
    1.10          fun excluded t =
    1.11            (* exclude numeric types: linear arithmetic subsumes transitivity *)
    1.12 @@ -350,7 +350,8 @@
    1.13  	      of NONE => NONE
    1.14  	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
    1.15            | dec x = rel x;
    1.16 -      in dec t end;
    1.17 +      in dec t end
    1.18 +      | decomp thy _ = NONE;
    1.19    in
    1.20      case s of
    1.21        "order" => Order_Tac.partial_tac decomp thms prems