diff -r b5b510c686cb -r f6d1ca0c6faf src/HOL/Imperative_HOL/Heap_Monad.thy --- 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((_))")