src/HOL/Tools/hologic.ML
changeset 38864 4abe644fcea5
parent 38857 97775f3e8722
child 39250 548a3e5521ab
     1.1 --- a/src/HOL/Tools/hologic.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/hologic.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -236,10 +236,10 @@
     1.4  fun dest_not (Const ("HOL.Not", _) $ t) = t
     1.5    | dest_not t = raise TERM ("dest_not", [t]);
     1.6  
     1.7 -fun eq_const T = Const ("op =", T --> T --> boolT);
     1.8 +fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
     1.9  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    1.10  
    1.11 -fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
    1.12 +fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
    1.13    | dest_eq t = raise TERM ("dest_eq", [t])
    1.14  
    1.15  fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);