# HG changeset patch
# User haftmann
# Date 1170758453 -3600
# Node ID 74ea64617c8988cd5a52b7d7fcf5ed4cb9fa39cc
# Parent  5bad0d4296942db572b45d4e0dfee074db913d8e
added eta expansion to imperative monad bind

diff -r 5bad0d429694 -r 74ea64617c89 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Feb 06 00:53:15 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Feb 06 11:40:53 2007 +0100
@@ -249,7 +249,15 @@
   let
     fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) vars fxy [t1, (v, ty) `|-> t2] =
           pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
-      | pretty _ _ _ _ = error "Bad arguments for imperative monad bind";
+      | pretty pr vars fxy [t1, t2] =
+          let
+            (*this code suffers from the lack of a proper concept for bindings*)
+            val vs = CodegenThingol.fold_varnames cons t2 [];
+            val v = Name.variant vs "x";
+            val vars' = CodegenNames.intro_vars [v] vars;
+            val var = IVar v;
+            val ty = "" `%% []; (*an approximation*)
+          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
   in (2, pretty) end;