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