syntax fix
authorhaftmann
Fri Aug 10 17:10:05 2007 +0200 (2007-08-10)
changeset 24224a5c95bbeb31d
parent 24223 fa9421d52c74
child 24225 348e982c694b
syntax fix
src/HOL/Library/State_Monad.thy
     1.1 --- a/src/HOL/Library/State_Monad.thy	Fri Aug 10 17:10:04 2007 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Aug 10 17:10:05 2007 +0200
     1.3 @@ -226,16 +226,16 @@
     1.4  
     1.5  print_translation {*
     1.6  let
     1.7 -  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
     1.8 +  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ Abs (abs as (_, ty, _))) =
     1.9          let
    1.10 -          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.11 -        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.12 +          val (v', g') = Syntax.variant_abs abs;
    1.13 +        in Const ("_mbind", dummyT) $ Free (v', ty) $ f $ unfold_monad g' end
    1.14      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
    1.15          Const ("_fcomp", dummyT) $ f $ unfold_monad g
    1.16 -    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.17 +    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ Abs (abs as (_, ty, _))) =
    1.18          let
    1.19 -          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.20 -        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.21 +          val (v', g') = Syntax.variant_abs abs;
    1.22 +        in Const ("_mbind", dummyT) $ Free (v', ty) $ f $ unfold_monad g' end
    1.23      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.24          Const ("return", dummyT) $ f
    1.25      | unfold_monad f = f;