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