tuned
authorhaftmann
Thu Aug 19 10:27:12 2010 +0200 (2010-08-19)
changeset 38548dea0d2cca822
parent 38547 973506fe2dbd
child 38549 d0385f2764d8
tuned
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Aug 19 10:27:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Aug 19 10:27:12 2010 +0200
     1.3 @@ -230,13 +230,13 @@
     1.4  
     1.5  fun disjuncts t = disjuncts_aux t [];
     1.6  
     1.7 -fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
     1.8 +fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
     1.9    | dest_imp  t = raise TERM ("dest_imp", [t]);
    1.10  
    1.11  fun dest_not (Const ("Not", _) $ t) = t
    1.12    | dest_not t = raise TERM ("dest_not", [t]);
    1.13  
    1.14 -fun eq_const T = Const ("op =", [T, T] ---> boolT);
    1.15 +fun eq_const T = Const ("op =", T --> T --> boolT);
    1.16  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    1.17  
    1.18  fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)