tuned ML setup;
authorwenzelm
Wed Feb 28 22:05:43 2007 +0100 (2007-02-28)
changeset 2237761610b1beedf
parent 22376 b711c2ad7507
child 22378 8e02a61b401f
tuned ML setup;
src/HOL/HOL.thy
src/HOL/Library/State_Monad.thy
src/HOL/Orderings.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Feb 28 22:05:41 2007 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Feb 28 22:05:43 2007 +0100
     1.3 @@ -217,11 +217,10 @@
     1.4  
     1.5  typed_print_translation {*
     1.6  let
     1.7 -  val thy = the_context ();
     1.8    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
     1.9      if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
    1.10      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    1.11 -in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end;
    1.12 +in map tr' [@{const_syntax "HOL.one"}, @{const_syntax "HOL.zero"}] end;
    1.13  *} -- {* show types that are presumably too general *}
    1.14  
    1.15  
    1.16 @@ -874,9 +873,7 @@
    1.17  declare exE [elim!]
    1.18    allE [elim]
    1.19  
    1.20 -ML {*
    1.21 -val HOL_cs = Classical.claset_of (the_context ());
    1.22 -*}
    1.23 +ML {* val HOL_cs = @{claset} *}
    1.24  
    1.25  lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
    1.26    apply (erule swap)
    1.27 @@ -1254,9 +1251,7 @@
    1.28  lemmas [cong] = imp_cong simp_implies_cong
    1.29  lemmas [split] = split_if
    1.30  
    1.31 -ML {*
    1.32 -val HOL_ss = Simplifier.simpset_of (the_context ());
    1.33 -*}
    1.34 +ML {* val HOL_ss = @{simpset} *}
    1.35  
    1.36  text {* Simplifies x assuming c and y assuming ~c *}
    1.37  lemma if_cong:
     2.1 --- a/src/HOL/Library/State_Monad.thy	Wed Feb 28 22:05:41 2007 +0100
     2.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Feb 28 22:05:43 2007 +0100
     2.3 @@ -87,9 +87,9 @@
     2.4  abbreviation (input)
     2.5    "return \<equiv> Pair"
     2.6  
     2.7 -print_ast_translation {*[
     2.8 -  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
     2.9 -]*}
    2.10 +print_ast_translation {*
    2.11 +  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
    2.12 +*}
    2.13  
    2.14  text {*
    2.15    Given two transformations @{term f} and @{term g}, they
    2.16 @@ -226,9 +226,8 @@
    2.17  
    2.18  print_translation {*
    2.19  let
    2.20 -  val syntax_name = Sign.const_syntax_name (the_context ());
    2.21 -  val name_mbind = syntax_name "State_Monad.mbind";
    2.22 -  val name_fcomp = syntax_name "State_Monad.fcomp";
    2.23 +  val name_mbind = @{const_syntax "mbind"};
    2.24 +  val name_fcomp = @{const_syntax "fcomp"};
    2.25    fun unfold_monad (t as Const (name, _) $ f $ g) =
    2.26          if name = name_mbind then let
    2.27              val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    2.28 @@ -246,9 +245,7 @@
    2.29      | unfold_monad f = f;
    2.30    fun tr' (f::ts) =
    2.31      list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
    2.32 -in [
    2.33 -  (syntax_name "State_Monad.run", tr')
    2.34 -] end;
    2.35 +in [(@{const_syntax "run"}, tr')] end;
    2.36  *}
    2.37  
    2.38  subsection {* Combinators *}
     3.1 --- a/src/HOL/Orderings.thy	Wed Feb 28 22:05:41 2007 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Wed Feb 28 22:05:43 2007 +0100
     3.3 @@ -517,14 +517,12 @@
     3.4  
     3.5  print_translation {*
     3.6  let
     3.7 -  val syntax_name = Sign.const_syntax_name (the_context ());
     3.8 -  val binder_name = Syntax.binder_name o syntax_name;
     3.9 -  val All_binder = binder_name "All";
    3.10 -  val Ex_binder = binder_name "Ex";
    3.11 -  val impl = syntax_name "op -->";
    3.12 -  val conj = syntax_name "op &";
    3.13 -  val less = syntax_name "Orderings.less";
    3.14 -  val less_eq = syntax_name "Orderings.less_eq";
    3.15 +  val All_binder = Syntax.binder_name @{const_syntax "All"};
    3.16 +  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
    3.17 +  val impl = @{const_syntax "op -->"};
    3.18 +  val conj = @{const_syntax "op &"};
    3.19 +  val less = @{const_syntax "less"};
    3.20 +  val less_eq = @{const_syntax "less_eq"};
    3.21  
    3.22    val trans =
    3.23     [((All_binder, impl, less), ("_All_less", "_All_greater")),
     4.1 --- a/src/HOL/Set.thy	Wed Feb 28 22:05:41 2007 +0100
     4.2 +++ b/src/HOL/Set.thy	Wed Feb 28 22:05:43 2007 +0100
     4.3 @@ -228,16 +228,13 @@
     4.4  
     4.5  print_translation {*
     4.6  let
     4.7 -  val thy = the_context ();
     4.8 -  val syntax_name = Sign.const_syntax_name thy;
     4.9 -  val set_type = Sign.intern_type thy "set";
    4.10 -  val binder_name = Syntax.binder_name o syntax_name;
    4.11 -  val All_binder = binder_name "All";
    4.12 -  val Ex_binder = binder_name "Ex";
    4.13 -  val impl = syntax_name "op -->";
    4.14 -  val conj = syntax_name "op &";
    4.15 -  val sbset = syntax_name "Set.subset";
    4.16 -  val sbset_eq = syntax_name "Set.subset_eq";
    4.17 +  val Type (set_type, _) = @{typ "'a set"};
    4.18 +  val All_binder = Syntax.binder_name @{const_syntax "All"};
    4.19 +  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
    4.20 +  val impl = @{const_syntax "op -->"};
    4.21 +  val conj = @{const_syntax "op &"};
    4.22 +  val sbset = @{const_syntax "subset"};
    4.23 +  val sbset_eq = @{const_syntax "subset_eq"};
    4.24  
    4.25    val trans =
    4.26     [((All_binder, impl, sbset), "_setlessAll"),