# HG changeset patch
# User haftmann
# Date 1285935349 -7200
# Node ID ff9e9d5ac17173edbe51a8d3b4554f9ebfbecb0a
# Parent  5228c6b2027374e89c88716791b42faf8f2951e5
use module integer for Eval

diff -r 5228c6b20273 -r ff9e9d5ac171 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Oct 01 11:46:09 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Oct 01 14:15:49 2010 +0200
@@ -340,7 +340,7 @@
   (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   (Haskell "divMod")
   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
-  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))")
 
 code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")