--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 05 07:10:51 2012 +0200
@@ -228,7 +228,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
(SML "IntInf.*/ ((_),/ (_))")
@@ -269,7 +269,7 @@
(SML "!(raise/ Fail/ \"num'_of'_nat\")")
(OCaml "failwith/ \"num'_of'_nat\"")
(Haskell "error/ \"num'_of'_nat\"")
- (Scala "!error(\"num'_of'_nat\")")
+ (Scala "!sys.error(\"num'_of'_nat\")")
subsection {* Evaluation *}