| changeset 48073 | 1b609a7837ef |
| parent 48072 | ace701efe203 |
| child 51143 | 0a2371e7ced3 |
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 05 07:05:56 2012 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 05 07:10:51 2012 +0200 @@ -610,7 +610,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 "!sys.error((_))") subsubsection {* Target variants with less units *}