src/HOL/Imperative_HOL/Ref.thy
changeset 37878 d016aaead7a2
parent 37845 b70d7a347964
child 37965 0c1743d31b5c
--- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 19 11:55:42 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 19 11:55:42 2010 +0200
@@ -296,11 +296,11 @@
 
 text {* Scala *}
 
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
+code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
 
 end