src/HOL/Library/State_Monad.thy
changeset 35115 446c5063e4fd
parent 31033 c46d52fee219
child 37751 89e16802b6cc
     1.1 --- a/src/HOL/Library/State_Monad.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -159,15 +159,15 @@
     1.4    fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
     1.5          let
     1.6            val (v, g') = dest_abs_eta g;
     1.7 -        in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
     1.8 +        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
     1.9      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
    1.10 -        Const ("_fcomp", dummyT) $ f $ unfold_monad g
    1.11 +        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
    1.12      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.13          let
    1.14            val (v, g') = dest_abs_eta g;
    1.15 -        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
    1.16 +        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
    1.17      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.18 -        Const ("return", dummyT) $ f
    1.19 +        Const (@{const_syntax "return"}, dummyT) $ f
    1.20      | unfold_monad f = f;
    1.21    fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
    1.22      | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
    1.23 @@ -175,18 +175,23 @@
    1.24      | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    1.25          contains_scomp t;
    1.26    fun scomp_monad_tr' (f::g::ts) = list_comb
    1.27 -    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
    1.28 -  fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
    1.29 -      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
    1.30 +    (Const (@{syntax_const "_do"}, dummyT) $
    1.31 +      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
    1.32 +  fun fcomp_monad_tr' (f::g::ts) =
    1.33 +    if contains_scomp g then list_comb
    1.34 +      (Const (@{syntax_const "_do"}, dummyT) $
    1.35 +        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
    1.36      else raise Match;
    1.37 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
    1.38 -      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    1.39 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
    1.40 +    if contains_scomp g' then list_comb
    1.41 +      (Const (@{syntax_const "_do"}, dummyT) $
    1.42 +        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    1.43      else raise Match;
    1.44 -in [
    1.45 -  (@{const_syntax scomp}, scomp_monad_tr'),
    1.46 +in
    1.47 + [(@{const_syntax scomp}, scomp_monad_tr'),
    1.48    (@{const_syntax fcomp}, fcomp_monad_tr'),
    1.49 -  (@{const_syntax Let}, Let_monad_tr')
    1.50 -] end;
    1.51 +  (@{const_syntax Let}, Let_monad_tr')]
    1.52 +end;
    1.53  *}
    1.54  
    1.55  text {*