# HG changeset patch
# User haftmann
# Date 1280135384 -7200
# Node ID 0c1743d31b5ce66e880e26b358c2a501b9a5d553
# Parent  0a1ae22df1f1042ed467878a10cf3bba90e3500f
modified namespace policy

diff -r 0a1ae22df1f1 -r 0c1743d31b5c src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 26 11:09:44 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 26 11:09:44 2010 +0200
@@ -299,8 +299,7 @@
 code_type ref (Scala "!Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
 code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
 
 end
-