src/HOL/Set.thy
changeset 42287 d98eb048a2e4
parent 42284 326f57825e1a
child 42455 6702c984bf5a
--- 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};