changeset 24253 3d7f74fd9fd9 parent 24224 a5c95bbeb31d child 25595 6c48275f9c76
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.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;