
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -306,10 +306,10 @@
 
 text {* Scala *}
 
-code_type ref (Scala "!Ref[_]")
+code_type ref (Scala "!Heap.Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
 
 end




