src/HOL/Library/State_Monad.thy
changeset 22377 61610b1beedf
parent 21835 84fd5de0691c
child 22492 43545e640877
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Feb 28 22:05:41 2007 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Feb 28 22:05:43 2007 +0100
     1.3 @@ -87,9 +87,9 @@
     1.4  abbreviation (input)
     1.5    "return \<equiv> Pair"
     1.6  
     1.7 -print_ast_translation {*[
     1.8 -  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
     1.9 -]*}
    1.10 +print_ast_translation {*
    1.11 +  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
    1.12 +*}
    1.13  
    1.14  text {*
    1.15    Given two transformations @{term f} and @{term g}, they
    1.16 @@ -226,9 +226,8 @@
    1.17  
    1.18  print_translation {*
    1.19  let
    1.20 -  val syntax_name = Sign.const_syntax_name (the_context ());
    1.21 -  val name_mbind = syntax_name "State_Monad.mbind";
    1.22 -  val name_fcomp = syntax_name "State_Monad.fcomp";
    1.23 +  val name_mbind = @{const_syntax "mbind"};
    1.24 +  val name_fcomp = @{const_syntax "fcomp"};
    1.25    fun unfold_monad (t as Const (name, _) $ f $ g) =
    1.26          if name = name_mbind then let
    1.27              val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.28 @@ -246,9 +245,7 @@
    1.29      | unfold_monad f = f;
    1.30    fun tr' (f::ts) =
    1.31      list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
    1.32 -in [
    1.33 -  (syntax_name "State_Monad.run", tr')
    1.34 -] end;
    1.35 +in [(@{const_syntax "run"}, tr')] end;
    1.36  *}
    1.37  
    1.38  subsection {* Combinators *}