# HG changeset patch
# User haftmann
# Date 1285747544 -7200
# Node ID 2053638a2bf298299fc760fa24d07d163f43519d
# Parent  2f43fffbba1acc1516181f7a3c5e4c4d61c7ee08
scala is reserved identifier

diff -r 2f43fffbba1a -r 2053638a2bf2 src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Wed Sep 29 09:21:26 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Wed Sep 29 10:05:44 2010 +0200
@@ -78,7 +78,7 @@
   def equals(that: Natural): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
-  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
+  def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
       this.value.intValue
     else error("Int value out of range: " + this.value.toString)
 
diff -r 2f43fffbba1a -r 2053638a2bf2 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 29 09:21:26 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Sep 29 10:05:44 2010 +0200
@@ -303,7 +303,7 @@
   def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
-  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
+  def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
       this.value.intValue
     else error("Int value out of range: " + this.value.toString)
 
diff -r 2f43fffbba1a -r 2053638a2bf2 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Sep 29 09:21:26 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 29 10:05:44 2010 +0200
@@ -430,7 +430,7 @@
       "true", "type", "val", "var", "while", "with", "yield"
     ]
   #> fold (Code_Target.add_reserved target) [
-      "apply", "error", "BigInt", "Nil", "List"
+      "apply", "error", "scala", "BigInt", "Nil", "List"
     ];
 
 end; (*struct*)