diff -r 24075ad39ca2 -r d98eb048a2e4 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Orderings.thy	Fri Apr 08 14:20:57 2011 +0200
@@ -638,8 +638,8 @@
 
 print_translation {*
 let
-  val All_binder = Syntax.binder_name @{const_syntax All};
-  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
+  val All_binder = Mixfix.binder_name @{const_syntax All};
+  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
   val impl = @{const_syntax HOL.implies};
   val conj = @{const_syntax HOL.conj};
   val less = @{const_syntax less};