src/HOL/IntDiv.thy

 in
 
 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   if n = 0 then NONE
   else
-    let val (k, l) = IntInf.divMod (m, n);
+    let val (k, l) = Integer.div_mod m n;
         fun mk_num x = HOLogic.mk_number HOLogic.intT x;
     in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
     end);
 
 end;