
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 *}
 




