1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 22:06:37 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 22:19:58 2010 +0100
     1.3 @@ -147,16 +147,16 @@
     1.4            val v_used = fold_aterms
     1.5              (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
     1.6          in if v_used then
     1.7 -          Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
     1.8 +          Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g'
     1.9          else
    1.10 -          Const ("_chainM", dummyT) $ f $ unfold_monad g'
    1.11 +          Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g'
    1.12          end
    1.13      | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
    1.14 -        Const ("_chainM", dummyT) $ f $ unfold_monad g
    1.15 +        Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g
    1.16      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.17          let
    1.18            val (v, g') = dest_abs_eta g;
    1.19 -        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
    1.20 +        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
    1.21      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.22          Const (@{const_syntax return}, dummyT) $ f
    1.23      | unfold_monad f = f;
    1.24 @@ -164,14 +164,17 @@
    1.25      | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    1.26          contains_bindM t;
    1.27    fun bindM_monad_tr' (f::g::ts) = list_comb
    1.28 -    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
    1.29 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
    1.30 -      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    1.31 +    (Const (@{syntax_const "_do"}, dummyT) $
    1.32 +      unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
    1.33 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
    1.34 +    if contains_bindM g' then list_comb
    1.35 +      (Const (@{syntax_const "_do"}, dummyT) $
    1.36 +        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    1.37      else raise Match;
    1.38 -in [
    1.39 -  (@{const_syntax bindM}, bindM_monad_tr'),
    1.40 -  (@{const_syntax Let}, Let_monad_tr')
    1.41 -] end;
    1.42 +in
    1.43 + [(@{const_syntax bindM}, bindM_monad_tr'),
    1.44 +  (@{const_syntax Let}, Let_monad_tr')]
    1.45 +end;
    1.46  *}
    1.47  
    1.48