# HG changeset patch
# User haftmann
# Date 1279533342 -7200
# Node ID d016aaead7a2a4116ded3f4e3b25733f7c05eaa8
# Parent  d4a30d21022058f6d8cb468aca6a3113a496c9f6
dropped superfluous prefixes

diff -r d4a30d210220 -r d016aaead7a2 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 19 11:55:42 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 19 11:55:42 2010 +0200
@@ -124,10 +124,10 @@
 *}  
 
 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
-  crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
+  crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
 
 lemma crelI:
-  "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
+  "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
   by (simp add: crel_def)
 
 lemma crelE:
@@ -300,9 +300,9 @@
   using assms by (auto simp add: crel_def bind_def split: option.split_asm)
 
 lemma execute_bind_eq_SomeI:
-  assumes "Heap_Monad.execute f h = Some (x, h')"
-    and "Heap_Monad.execute (g x) h' = Some (y, h'')"
-  shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
+  assumes "execute f h = Some (x, h')"
+    and "execute (g x) h' = Some (y, h'')"
+  shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
   using assms by (simp add: bind_def)
 
 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
@@ -487,7 +487,7 @@
 code_reserved Scala Heap
 
 code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "!Heap.bind((_), (_))")
+code_const bind (Scala "bind")
 code_const return (Scala "('_: Unit)/ =>/ _")
 code_const Heap_Monad.raise' (Scala "!error((_))")
 
diff -r d4a30d210220 -r d016aaead7a2 src/HOL/Imperative_HOL/Ref.thy
--- 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
 
diff -r d4a30d210220 -r d016aaead7a2 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 19 11:55:42 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 19 11:55:42 2010 +0200
@@ -337,7 +337,7 @@
 
 code_type nat
   (Haskell "Nat.Nat")
-  (Scala "Nat.Nat")
+  (Scala "Nat")
 
 code_instance nat :: eq
   (Haskell -)
@@ -405,7 +405,7 @@
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
-  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
+  (Scala "!_.as'_BigInt" and "Nat")
 
 text {* Conversion from and to indices. *}
 
@@ -419,7 +419,7 @@
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "toEnum")
-  (Scala "!Nat.Nat((_))")
+  (Scala "Nat")
 
 text {* Using target language arithmetic operations whenever appropriate *}