src/HOL/Imperative_HOL/Heap_Monad.thy

 readArray = Data.Array.ST.readArray
 
 writeArray :: STArray s a -> Integer -> a -> ST s ()
 writeArray = Data.Array.ST.writeArray\<close>
 
-code_reserved Haskell Heap
+code_reserved (Haskell) Heap
 
 text \<open>Monad\<close>
 
 code_printing type_constructor Heap \<rightharpoonup> (Haskell) "Heap.ST/ Heap.RealWorld/ _"
 code_monad bind Haskell

   def freeze[A](a: T[A]): List[A] = a.toList
 }
 
 \<close>
 
-code_reserved Scala Heap Ref Array
+code_reserved (Scala) Heap Ref Array
 
 code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
 code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
 code_printing constant return \<rightharpoonup> (Scala) "('_: Unit)/ =>/ _"
 code_printing constant Heap_Monad.raise \<rightharpoonup> (Scala) "!sys.error((_))"