src/HOL/Imperative_HOL/Ref.thy
changeset 38968 e55deaa22fff
parent 38771 f9cd27cbe8a4
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 01 09:03:34 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 01 11:09:50 2010 +0200
     1.3 @@ -306,10 +306,10 @@
     1.4  
     1.5  text {* Scala *}
     1.6  
     1.7 -code_type ref (Scala "!Heap.Ref[_]")
     1.8 +code_type ref (Scala "!Ref[_]")
     1.9  code_const Ref (Scala "!error(\"bare Ref\")")
    1.10 -code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
    1.11 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
    1.12 -code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
    1.13 +code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
    1.14 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
    1.15 +code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
    1.16  
    1.17  end