scala is reserved identifier
authorhaftmann
Wed Sep 29 10:05:44 2010 +0200 (2010-09-29)
changeset 397812053638a2bf2
parent 39780 2f43fffbba1a
child 39782 f75381bc46d2
child 39783 a8c52b982ff2
scala is reserved identifier
src/HOL/Library/Code_Natural.thy
src/HOL/Library/Efficient_Nat.thy
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Library/Code_Natural.thy	Wed Sep 29 09:21:26 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Wed Sep 29 10:05:44 2010 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4    def equals(that: Natural): Boolean = this.value == that.value
     1.5  
     1.6    def as_BigInt: BigInt = this.value
     1.7 -  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
     1.8 +  def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
     1.9        this.value.intValue
    1.10      else error("Int value out of range: " + this.value.toString)
    1.11  
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 29 09:21:26 2010 +0200
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Sep 29 10:05:44 2010 +0200
     2.3 @@ -303,7 +303,7 @@
     2.4    def equals(that: Nat): Boolean = this.value == that.value
     2.5  
     2.6    def as_BigInt: BigInt = this.value
     2.7 -  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
     2.8 +  def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
     2.9        this.value.intValue
    2.10      else error("Int value out of range: " + this.value.toString)
    2.11  
     3.1 --- a/src/Tools/Code/code_scala.ML	Wed Sep 29 09:21:26 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Wed Sep 29 10:05:44 2010 +0200
     3.3 @@ -430,7 +430,7 @@
     3.4        "true", "type", "val", "var", "while", "with", "yield"
     3.5      ]
     3.6    #> fold (Code_Target.add_reserved target) [
     3.7 -      "apply", "error", "BigInt", "Nil", "List"
     3.8 +      "apply", "error", "scala", "BigInt", "Nil", "List"
     3.9      ];
    3.10  
    3.11  end; (*struct*)