fixed syntax
authorhaftmann
Mon Aug 13 21:22:42 2007 +0200 (2007-08-13)
changeset 242533d7f74fd9fd9
parent 24252 4eb5bc6af008
child 24254 5180e11e4e42
fixed syntax
src/HOL/Library/State_Monad.thy
     1.1 --- a/src/HOL/Library/State_Monad.thy	Mon Aug 13 21:22:41 2007 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Aug 13 21:22:42 2007 +0200
     1.3 @@ -226,16 +226,24 @@
     1.4  
     1.5  print_translation {*
     1.6  let
     1.7 -  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ Abs (abs as (_, ty, _))) =
     1.8 +  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
     1.9 +        let
    1.10 +          val (v, t) = Syntax.variant_abs abs;
    1.11 +        in ((v, ty), t) end
    1.12 +    | dest_abs_eta t =
    1.13          let
    1.14 -          val (v', g') = Syntax.variant_abs abs;
    1.15 -        in Const ("_mbind", dummyT) $ Free (v', ty) $ f $ unfold_monad g' end
    1.16 +          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    1.17 +        in ((v, dummyT), t) end
    1.18 +  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
    1.19 +        let
    1.20 +          val ((v, ty), g') = dest_abs_eta g;
    1.21 +        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.22      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
    1.23          Const ("_fcomp", dummyT) $ f $ unfold_monad g
    1.24 -    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ Abs (abs as (_, ty, _))) =
    1.25 +    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.26          let
    1.27 -          val (v', g') = Syntax.variant_abs abs;
    1.28 -        in Const ("_mbind", dummyT) $ Free (v', ty) $ f $ unfold_monad g' end
    1.29 +          val ((v, ty), g') = dest_abs_eta g;
    1.30 +        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.31      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.32          Const ("return", dummyT) $ f
    1.33      | unfold_monad f = f;