--- a/src/HOL/Tools/TFL/dcterm.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Thu Aug 26 20:51:17 2010 +0200
@@ -128,7 +128,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_imp = dest_binop @{const_name "op -->"}
+val dest_imp = dest_binop @{const_name HOL.implies}
val dest_conj = dest_binop @{const_name "op &"}
val dest_disj = dest_binop @{const_name "op |"}
val dest_select = dest_binder @{const_name Eps}