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