src/HOL/Library/State_Monad.thy

   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   "_nil f" => "f"
 
 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;
   fun tr' (f::ts) =
     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)