diff -r 053c69cb4a0e -r 4abe644fcea5 src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/TFL/dcterm.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -127,7 +127,7 @@
 
 val dest_neg    = dest_monop @{const_name Not}
 val dest_pair   = dest_binop @{const_name Pair}
-val dest_eq     = dest_binop @{const_name "op ="}
+val dest_eq     = dest_binop @{const_name HOL.eq}
 val dest_imp    = dest_binop @{const_name HOL.implies}
 val dest_conj   = dest_binop @{const_name HOL.conj}
 val dest_disj   = dest_binop @{const_name HOL.disj}