changeset 49088 | 1b609a7837ef |
parent 48088 | 501b9bbd0d6e |
child 49446 | 6efff142bb54 |
1.1 --- a/src/HOL/Library/Code_Integer.thy Tue Jun 05 07:05:56 2012 +0200 1.2 +++ b/src/HOL/Library/Code_Integer.thy Tue Jun 05 07:10:51 2012 +0200 1.3 @@ -111,7 +111,7 @@ 1.4 (SML "!(raise/ Fail/ \"sub\")") 1.5 (OCaml "failwith/ \"sub\"") 1.6 (Haskell "error/ \"sub\"") 1.7 - (Scala "!error(\"sub\")") 1.8 + (Scala "!sys.error(\"sub\")") 1.9 1.10 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" 1.11 (SML "IntInf.* ((_), (_))")