--- 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};