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