# HG changeset patch
# User haftmann
# Date 1282206432 -7200
# Node ID dea0d2cca822ba80b10bbe7487f7d60669f4f93b
# Parent  973506fe2dbd358348b37cda95e656fb6b7fa304
tuned

diff -r 973506fe2dbd -r dea0d2cca822 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Aug 19 10:27:02 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Aug 19 10:27:12 2010 +0200
@@ -230,13 +230,13 @@
 
 fun disjuncts t = disjuncts_aux t [];
 
-fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
+fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
 fun dest_not (Const ("Not", _) $ t) = t
   | dest_not t = raise TERM ("dest_not", [t]);
 
-fun eq_const T = Const ("op =", [T, T] ---> boolT);
+fun eq_const T = Const ("op =", T --> T --> boolT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)