1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 01 09:03:34 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Sep 01 11:09:50 2010 +0200
     1.3 @@ -281,9 +281,7 @@
     1.4  code_reserved Haskell Nat
     1.5  
     1.6  code_include Scala "Nat"
     1.7 -{*import scala.Math
     1.8 -
     1.9 -object Nat {
    1.10 +{*object Nat {
    1.11  
    1.12    def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    1.13    def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    1.14 @@ -330,7 +328,7 @@
    1.15  
    1.16  code_type nat
    1.17    (Haskell "Nat.Nat")
    1.18 -  (Scala "Nat.Nat")
    1.19 +  (Scala "Nat")
    1.20  
    1.21  code_instance nat :: equal
    1.22    (Haskell -)
    1.23 @@ -397,7 +395,7 @@
    1.24  
    1.25  code_const int and nat
    1.26    (Haskell "toInteger" and "fromInteger")
    1.27 -  (Scala "!_.as'_BigInt" and "Nat.Nat")
    1.28 +  (Scala "!_.as'_BigInt" and "Nat")
    1.29  
    1.30  text {* Conversion from and to code numerals. *}
    1.31  
    1.32 @@ -405,14 +403,14 @@
    1.33    (SML "IntInf.toInt")
    1.34    (OCaml "_")
    1.35    (Haskell "!(fromInteger/ ./ toInteger)")
    1.36 -  (Scala "!Natural.Nat(_.as'_BigInt)")
    1.37 +  (Scala "!Natural(_.as'_BigInt)")
    1.38    (Eval "_")
    1.39  
    1.40  code_const Code_Numeral.nat_of
    1.41    (SML "IntInf.fromInt")
    1.42    (OCaml "_")
    1.43    (Haskell "!(fromInteger/ ./ toInteger)")
    1.44 -  (Scala "!Nat.Nat(_.as'_BigInt)")
    1.45 +  (Scala "!Nat(_.as'_BigInt)")
    1.46    (Eval "_")
    1.47  
    1.48  text {* Using target language arithmetic operations whenever appropriate *}