src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Orderings.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -640,7 +640,7 @@
 let
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
-  val impl = @{const_syntax "op -->"};
+  val impl = @{const_syntax HOL.implies};
   val conj = @{const_syntax "op &"};
   val less = @{const_syntax less};
   val less_eq = @{const_syntax less_eq};