src/HOL/Orderings.thy
changeset 42287 d98eb048a2e4
parent 42284 326f57825e1a
child 42795 66fcc9882784
     1.1 --- a/src/HOL/Orderings.thy	Fri Apr 08 14:05:31 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Apr 08 14:20:57 2011 +0200
     1.3 @@ -638,8 +638,8 @@
     1.4  
     1.5  print_translation {*
     1.6  let
     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 less = @{const_syntax less};