# HG changeset patch
# User wenzelm
# Date 1172696743 -3600
# Node ID 61610b1beedfb5dce3979ada9220186aded2cf59
# Parent  b711c2ad750759bad9a1b27521008455d02c2050
tuned ML setup;

diff -r b711c2ad7507 -r 61610b1beedf src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Feb 28 22:05:41 2007 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 28 22:05:43 2007 +0100
@@ -217,11 +217,10 @@
 
 typed_print_translation {*
 let
-  val thy = the_context ();
   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
     if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end;
+in map tr' [@{const_syntax "HOL.one"}, @{const_syntax "HOL.zero"}] end;
 *} -- {* show types that are presumably too general *}
 
 
@@ -874,9 +873,7 @@
 declare exE [elim!]
   allE [elim]
 
-ML {*
-val HOL_cs = Classical.claset_of (the_context ());
-*}
+ML {* val HOL_cs = @{claset} *}
 
 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   apply (erule swap)
@@ -1254,9 +1251,7 @@
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = split_if
 
-ML {*
-val HOL_ss = Simplifier.simpset_of (the_context ());
-*}
+ML {* val HOL_ss = @{simpset} *}
 
 text {* Simplifies x assuming c and y assuming ~c *}
 lemma if_cong:
diff -r b711c2ad7507 -r 61610b1beedf src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Feb 28 22:05:41 2007 +0100
+++ b/src/HOL/Library/State_Monad.thy	Wed Feb 28 22:05:43 2007 +0100
@@ -87,9 +87,9 @@
 abbreviation (input)
   "return \<equiv> Pair"
 
-print_ast_translation {*[
-  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
-]*}
+print_ast_translation {*
+  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
+*}
 
 text {*
   Given two transformations @{term f} and @{term g}, they
@@ -226,9 +226,8 @@
 
 print_translation {*
 let
-  val syntax_name = Sign.const_syntax_name (the_context ());
-  val name_mbind = syntax_name "State_Monad.mbind";
-  val name_fcomp = syntax_name "State_Monad.fcomp";
+  val name_mbind = @{const_syntax "mbind"};
+  val name_fcomp = @{const_syntax "fcomp"};
   fun unfold_monad (t as Const (name, _) $ f $ g) =
         if name = name_mbind then let
             val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
@@ -246,9 +245,7 @@
     | unfold_monad f = f;
   fun tr' (f::ts) =
     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
-in [
-  (syntax_name "State_Monad.run", tr')
-] end;
+in [(@{const_syntax "run"}, tr')] end;
 *}
 
 subsection {* Combinators *}
diff -r b711c2ad7507 -r 61610b1beedf src/HOL/Orderings.thy
--- 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")),
diff -r b711c2ad7507 -r 61610b1beedf src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Feb 28 22:05:41 2007 +0100
+++ b/src/HOL/Set.thy	Wed Feb 28 22:05:43 2007 +0100
@@ -228,16 +228,13 @@
 
 print_translation {*
 let
-  val thy = the_context ();
-  val syntax_name = Sign.const_syntax_name thy;
-  val set_type = Sign.intern_type thy "set";
-  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 sbset = syntax_name "Set.subset";
-  val sbset_eq = syntax_name "Set.subset_eq";
+  val Type (set_type, _) = @{typ "'a set"};
+  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 sbset = @{const_syntax "subset"};
+  val sbset_eq = @{const_syntax "subset_eq"};
 
   val trans =
    [((All_binder, impl, sbset), "_setlessAll"),