src/HOL/Orderings.thy
changeset 22377 61610b1beedf
parent 22348 ab505d281015
child 22384 33a46e6c7f04
--- a/src/HOL/Orderings.thy	Wed Feb 28 22:05:41 2007 +0100
+++ b/src/HOL/Orderings.thy	Wed Feb 28 22:05:43 2007 +0100
@@ -517,14 +517,12 @@
 
 print_translation {*
 let
-  val syntax_name = Sign.const_syntax_name (the_context ());
-  val binder_name = Syntax.binder_name o syntax_name;
-  val All_binder = binder_name "All";
-  val Ex_binder = binder_name "Ex";
-  val impl = syntax_name "op -->";
-  val conj = syntax_name "op &";
-  val less = syntax_name "Orderings.less";
-  val less_eq = syntax_name "Orderings.less_eq";
+  val All_binder = Syntax.binder_name @{const_syntax "All"};
+  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
+  val impl = @{const_syntax "op -->"};
+  val conj = @{const_syntax "op &"};
+  val less = @{const_syntax "less"};
+  val less_eq = @{const_syntax "less_eq"};
 
   val trans =
    [((All_binder, impl, less), ("_All_less", "_All_greater")),