changeset 48073 | 1b609a7837ef |
parent 47217 | 501b9bbd0d6e |
child 48431 | 6efff142bb54 |
--- a/src/HOL/Library/Code_Integer.thy Tue Jun 05 07:05:56 2012 +0200 +++ b/src/HOL/Library/Code_Integer.thy Tue Jun 05 07:10:51 2012 +0200 @@ -111,7 +111,7 @@ (SML "!(raise/ Fail/ \"sub\")") (OCaml "failwith/ \"sub\"") (Haskell "error/ \"sub\"") - (Scala "!error(\"sub\")") + (Scala "!sys.error(\"sub\")") code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" (SML "IntInf.* ((_), (_))")