src/HOL/Orderings.thy
changeset 22377 61610b1beedf
parent 22348 ab505d281015
child 22384 33a46e6c7f04
     1.1 --- a/src/HOL/Orderings.thy	Wed Feb 28 22:05:41 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Feb 28 22:05:43 2007 +0100
     1.3 @@ -517,14 +517,12 @@
     1.4  
     1.5  print_translation {*
     1.6  let
     1.7 -  val syntax_name = Sign.const_syntax_name (the_context ());
     1.8 -  val binder_name = Syntax.binder_name o syntax_name;
     1.9 -  val All_binder = binder_name "All";
    1.10 -  val Ex_binder = binder_name "Ex";
    1.11 -  val impl = syntax_name "op -->";
    1.12 -  val conj = syntax_name "op &";
    1.13 -  val less = syntax_name "Orderings.less";
    1.14 -  val less_eq = syntax_name "Orderings.less_eq";
    1.15 +  val All_binder = Syntax.binder_name @{const_syntax "All"};
    1.16 +  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
    1.17 +  val impl = @{const_syntax "op -->"};
    1.18 +  val conj = @{const_syntax "op &"};
    1.19 +  val less = @{const_syntax "less"};
    1.20 +  val less_eq = @{const_syntax "less_eq"};
    1.21  
    1.22    val trans =
    1.23     [((All_binder, impl, less), ("_All_less", "_All_greater")),