src/HOL/Tools/Qelim/qelim.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 41453 c03593812297
     1.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4      Const(s,T)$_$_ => 
     1.5         if domain_type T = HOLogic.boolT
     1.6            andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
     1.7 -            @{const_name HOL.implies}, @{const_name "op ="}] s
     1.8 +            @{const_name HOL.implies}, @{const_name HOL.eq}] s
     1.9         then binop_conv (conv env) p 
    1.10         else atcv env p
    1.11    | Const(@{const_name Not},_)$_ => arg_conv (conv env) p