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