diff -r 28848d338261 -r 27e7047d9ae6 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 10:23:21 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 13:58:29 2010 +0200
@@ -469,14 +469,26 @@
 
 subsubsection {* Scala *}
 
-code_include Haskell "Heap"
-{*def bind[A, B](f: Unit => A, g: A => Unit => B, u: Unit): B = g (f ()) ()*}
+code_include Scala "Heap"
+{*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+
+class Ref[A](x: A) {
+  var value = x
+}
+
+object Ref {
+  def apply[A](x: A): Ref[A] = new Ref[A](x)
+}
+
+def lookup[A](r: Ref[A]): A = r.value
+
+def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
 
 code_reserved Scala Heap
 
 code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "Heap.bind")
-code_const return (Scala "!(()/ =>/ _)")
+code_const bind (Scala "!Heap.bind((_), (_))")
+code_const return (Scala "('_: Unit)/ =>/ _")
 code_const Heap_Monad.raise' (Scala "!error(_)")