
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -330,7 +330,7 @@
 
 code_type nat
   (Haskell "Nat.Nat")
-  (Scala "Nat")
+  (Scala "Nat.Nat")
 
 code_instance nat :: eq
   (Haskell -)
@@ -397,7 +397,7 @@
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
-  (Scala "!_.as'_BigInt" and "Nat")
+  (Scala "!_.as'_BigInt" and "Nat.Nat")
 
 text {* Conversion from and to code numerals. *}
 
@@ -405,14 +405,14 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Natural(_.as'_BigInt)")
+  (Scala "!Natural.Nat(_.as'_BigInt)")
   (Eval "_")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Nat(_.as'_BigInt)")
+  (Scala "!Nat.Nat(_.as'_BigInt)")
   (Eval "_")
 
 text {* Using target language arithmetic operations whenever appropriate *}




