| changeset 37845 | b70d7a347964 |
| parent 37842 | 27e7047d9ae6 |
| child 37878 | d016aaead7a2 |
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 16 14:11:08 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 16 15:28:22 2010 +0200 @@ -489,7 +489,7 @@ code_type Heap (Scala "Unit/ =>/ _") code_const bind (Scala "!Heap.bind((_), (_))") code_const return (Scala "('_: Unit)/ =>/ _") -code_const Heap_Monad.raise' (Scala "!error(_)") +code_const Heap_Monad.raise' (Scala "!error((_))") subsubsection {* Target variants with less units *}