--- a/src/HOL/Set.thy Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Set.thy Fri Apr 08 14:20:57 2011 +0200
@@ -231,8 +231,8 @@
print_translation {*
let
val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *)
- 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 sbset = @{const_syntax subset};