# HG changeset patch
# User haftmann
# Date 1186758605 -7200
# Node ID a5c95bbeb31dccccad5b5faaf138e6dcf6e87c65
# Parent  fa9421d52c74b9e3b04b62a6a9d7f6f4bf326ee2
syntax fix

diff -r fa9421d52c74 -r a5c95bbeb31d src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Fri Aug 10 17:10:04 2007 +0200
+++ b/src/HOL/Library/State_Monad.thy	Fri Aug 10 17:10:05 2007 +0200
@@ -226,16 +226,16 @@
 
 print_translation {*
 let
-  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
+  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ Abs (abs as (_, ty, _))) =
         let
-          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
-        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+          val (v', g') = Syntax.variant_abs abs;
+        in Const ("_mbind", dummyT) $ Free (v', ty) $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
         Const ("_fcomp", dummyT) $ f $ unfold_monad g
-    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
+    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ Abs (abs as (_, ty, _))) =
         let
-          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
-        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+          val (v', g') = Syntax.variant_abs abs;
+        in Const ("_mbind", dummyT) $ Free (v', ty) $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
         Const ("return", dummyT) $ f
     | unfold_monad f = f;