--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 18 10:04:06 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 18 15:35:53 2013 +0200
@@ -556,12 +556,12 @@
subsubsection {* SML and OCaml *}
-code_type Heap (SML "unit/ ->/ _")
+code_type Heap (SML "(unit/ ->/ _)")
code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
code_const return (SML "!(fn/ ()/ =>/ _)")
code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
-code_type Heap (OCaml "unit/ ->/ _")
+code_type Heap (OCaml "(unit/ ->/ _)")
code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
code_const return (OCaml "!(fun/ ()/ ->/ _)")
code_const Heap_Monad.raise' (OCaml "failwith")
@@ -653,7 +653,7 @@
code_reserved Scala Heap Ref Array
-code_type Heap (Scala "Unit/ =>/ _")
+code_type Heap (Scala "(Unit/ =>/ _)")
code_const bind (Scala "Heap.bind")
code_const return (Scala "('_: Unit)/ =>/ _")
code_const Heap_Monad.raise' (Scala "!sys.error((_))")