--- a/src/HOL/Decision_Procs/MIR.thy Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Aug 26 20:51:17 2010 +0200
@@ -5841,7 +5841,7 @@
@{code And} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op |"} $ t1 $ t2) =
@{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')