1.1 --- a/src/HOL/Set.thy	Fri Apr 08 14:05:31 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Apr 08 14:20:57 2011 +0200
     1.3 @@ -231,8 +231,8 @@
     1.4  print_translation {*
     1.5  let
     1.6    val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
     1.7 -  val All_binder = Syntax.binder_name @{const_syntax All};
     1.8 -  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
     1.9 +  val All_binder = Mixfix.binder_name @{const_syntax All};
    1.10 +  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
    1.11    val impl = @{const_syntax HOL.implies};
    1.12    val conj = @{const_syntax HOL.conj};
    1.13    val sbset = @{const_syntax subset};