corrected ML semantics

--- a/src/HOL/Library/Array.thy	Sat Apr 26 13:20:16 2008 +0200
+++ b/src/HOL/Library/Array.thy	Sun Apr 27 17:13:01 2008 +0200
@@ -171,12 +171,12 @@
 
 code_type array (SML "_/ array")
 code_const Array (SML "raise/ (Fail/ \"bare Array\")")
-code_const Array.new' (SML "Array.array ((_), (_))")
-code_const Array.of_list (SML "Array.fromList")
-code_const Array.make' (SML "Array.tabulate ((_), (_))")
-code_const Array.length' (SML "Array.length")
-code_const Array.nth' (SML "Array.sub ((_), (_))")
-code_const Array.upd' (SML "Array.update ((_), (_), (_))")
+code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
+code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
+code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
+code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
+code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
+code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
 
 code_reserved SML Array
 
@@ -185,12 +185,12 @@
 
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "Array.make")
-code_const Array.of_list (OCaml "Array.of_list")
-code_const Array.make' (OCaml "Array.init")
-code_const Array.length' (OCaml "Array.length")
-code_const Array.nth' (OCaml "Array.get")
-code_const Array.upd' (OCaml "Array.set")
+code_const Array.new' (OCaml "(fn/ ()/ =>/ Array.make/ _/ _)")
+code_const Array.of_list (OCaml "(fn/ ()/ =>/ Array.of'_list/ _)")
+code_const Array.make' (OCaml "(fn/ ()/ =>/ Array.init/ _/ _)")
+code_const Array.length' (OCaml "(fn/ ()/ =>/ Array.length/ _)")
+code_const Array.nth' (OCaml "(fn/ ()/ =>/ Array.get/ _/ _)")
+code_const Array.upd' (OCaml "(fn/ ()/ =>/ Array.set/ _/ _/ _)")
 
 code_reserved OCaml Array
 
@@ -205,5 +205,4 @@
 code_const Array.nth' (Haskell "readArray")
 code_const Array.upd' (Haskell "writeArray")
 
-
 end

--- a/src/HOL/Library/Heap_Monad.thy	Sat Apr 26 13:20:16 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy	Sun Apr 27 17:13:01 2008 +0200
@@ -298,24 +298,25 @@
 
 subsubsection {* SML *}
 
-code_type Heap (SML "_")
+code_type Heap (SML "unit/ ->/ _")
+term "op \<guillemotright>="
 code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
-code_monad run "op \<guillemotright>=" SML
+code_monad run "op \<guillemotright>=" "()" SML
 code_const run (SML "_")
-code_const return (SML "_")
+code_const return (SML "(fn/ ()/ =>/ _)")
 code_const "Heap_Monad.Fail" (SML "Fail")
-code_const "Heap_Monad.raise_exc" (SML "raise")
+code_const "Heap_Monad.raise_exc" (SML "(fn/ ()/ =>/ raise/ _)")
 
 
 subsubsection {* OCaml *}
 
 code_type Heap (OCaml "_")
 code_const Heap (OCaml "failwith/ \"bare Heap\"")
-code_monad run "op \<guillemotright>=" OCaml
+code_monad run "op \<guillemotright>=" "()" OCaml
 code_const run (OCaml "_")
-code_const return (OCaml "_")
+code_const return (OCaml "(fn/ ()/ =>/ _)")
 code_const "Heap_Monad.Fail" (OCaml "Failure")
-code_const "Heap_Monad.raise_exc" (OCaml "raise")
+code_const "Heap_Monad.raise_exc" (OCaml "(fn/ ()/ =>/ raise/ _)")
 
 code_reserved OCaml Failure raise
 
@@ -366,7 +367,7 @@
 code_type Heap (Haskell "ST '_s _")
 code_const Heap (Haskell "error \"bare Heap\")")
 code_const evaluate (Haskell "runST")
-code_monad run bindM Haskell
+code_monad run "op \<guillemotright>=" Haskell
 code_const return (Haskell "return")
 code_const "Heap_Monad.Fail" (Haskell "_")
 code_const "Heap_Monad.raise_exc" (Haskell "error")

--- a/src/HOL/Library/Ref.thy	Sat Apr 26 13:20:16 2008 +0200
+++ b/src/HOL/Library/Ref.thy	Sun Apr 27 17:13:01 2008 +0200
@@ -62,9 +62,9 @@
 
 code_type ref (SML "_/ ref")
 code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
-code_const Ref.new (SML "ref")
-code_const Ref.lookup (SML "'!")
-code_const Ref.update (SML infixl 3 ":=")
+code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)")
+code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
+code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
 
 code_reserved SML ref
 
@@ -72,10 +72,10 @@
 subsubsection {* OCaml *}
 
 code_type ref (OCaml "_/ ref")
-code_const Ref (OCaml "failwith/ \"bare Ref\"")
-code_const Ref.new (OCaml "ref")
-code_const Ref.lookup (OCaml "'!")
-code_const Ref.update (OCaml infixr 1 ":=")
+code_const Ref (OCaml "failwith/ \"bare Ref\")")
+code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)")
+code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
+code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
 
 code_reserved OCaml ref
 

--- a/src/Tools/code/code_target.ML	Sat Apr 26 13:20:16 2008 +0200
+++ b/src/Tools/code/code_target.ML	Sun Apr 27 17:13:01 2008 +0200
@@ -1855,8 +1855,13 @@
         | NONE => error "Illegal message expression";
   in (1, pretty) end;
 
-fun pretty_imperative_monad_bind bind' =
+fun pretty_imperative_monad_bind bind' unit' =
   let
+    val dummy_name = "";
+    val dummy_type = ITyVar dummy_name;
+    val dummy_case_term = IVar dummy_name;
+    (*assumption: dummy values are not relevant for serialization*)
+    val unitt = IConst (unit', ([], []));
     fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
       | dest_abs (t, ty) =
           let
@@ -1864,16 +1869,18 @@
             val v = Name.variant vs "x";
             val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
           in ((v, ty'), t `$ IVar v) end;
-    fun tr_bind [(t1, _), (t2, ty2)] =
+    fun tr_bind' [(t1, _), (t2, ty2)] =
       let
         val ((v, ty), t) = dest_abs (t2, ty2);
-      in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end
-    and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t
+      in ICase (((t1 `$ unitt, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
+    and tr_bind'' (t as _ `$ _) = (case CodeThingol.unfold_app t
          of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
-              then tr_bind [(x1, ty1), (x2, ty2)]
-              else t
-          | _ => t)
-      | tr_bind' t = t;
+              then tr_bind' [(x1, ty1), (x2, ty2)]
+              else t `$ unitt
+          | _ => t `$ unitt)
+      | tr_bind'' t = t `$ unitt;
+    fun tr_bind ts = (dummy_name, dummy_type)
+      `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
     fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
   in (2, pretty) end;
 
@@ -2002,11 +2009,19 @@
 fun add_modl_alias target =
   map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
 
-fun add_monad target c_run c_bind thy =
+fun add_monad target c_run c_bind c_unit thy =
   let
     val c_run' = CodeUnit.read_const thy c_run;
     val c_bind' = CodeUnit.read_const thy c_bind;
     val c_bind'' = CodeName.const thy c_bind';
+    val c_unit'' = Option.map (CodeName.const thy o CodeUnit.read_const thy) c_unit;
+    val is_haskell = target = target_Haskell;
+    val _ = if is_haskell andalso is_some c_unit''
+      then error ("No unit entry may be given for Haskell monad")
+      else ();
+    val _ = if not is_haskell andalso is_none c_unit''
+      then error ("Unit entry must be given for SML/OCaml monad")
+      else ();
   in if target = target_Haskell then
     thy
     |> gen_add_syntax_const (K I) target_Haskell c_run'
@@ -2016,7 +2031,7 @@
   else
     thy
     |> gen_add_syntax_const (K I) target c_bind'
-          (SOME (pretty_imperative_monad_bind c_bind''))
+          (SOME (pretty_imperative_monad_bind c_bind'' (the c_unit'')))
   end;
 
 fun gen_allow_exception prep_cs raw_c thy =
@@ -2170,9 +2185,10 @@
 
 val _ =
   OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
-    P.term -- P.term -- Scan.repeat1 P.name
-    >> (fn ((raw_run, raw_bind), targets) => Toplevel.theory 
-          (fold (fn target => add_monad target raw_run raw_bind) targets))
+    P.term -- P.term -- ((P.term >> SOME) -- Scan.repeat1 P.name
+      || Scan.succeed NONE -- Scan.repeat1 P.name)
+    >> (fn ((raw_run, raw_bind), (raw_unit, targets)) => Toplevel.theory 
+          (fold (fn target => add_monad target raw_run raw_bind raw_unit) targets))
   );
 
 val _ =