--- a/src/HOL/Tools/simpdata.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Aug 26 20:51:17 2010 +0200
@@ -14,7 +14,7 @@
| dest_eq _ = NONE;
fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
- fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
| dest_imp _ = NONE;
val conj = HOLogic.conj
val imp = HOLogic.imp
@@ -159,7 +159,7 @@
(Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
+ [(@{const_name HOL.implies}, [@{thm mp}]),
(@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]),
(@{const_name True}, []),