src/HOL/Tools/TFL/dcterm.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 41164 6854e9a40edc
     1.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  val dest_neg    = dest_monop @{const_name Not}
     1.6  val dest_pair   = dest_binop @{const_name Pair}
     1.7 -val dest_eq     = dest_binop @{const_name "op ="}
     1.8 +val dest_eq     = dest_binop @{const_name HOL.eq}
     1.9  val dest_imp    = dest_binop @{const_name HOL.implies}
    1.10  val dest_conj   = dest_binop @{const_name HOL.conj}
    1.11  val dest_disj   = dest_binop @{const_name HOL.disj}