# HG changeset patch
# User wenzelm
# Date 1609518904 -3600
# Node ID b51515722274e630ba335bb7af308d71cfce3868
# Parent  05e2cab9af8bd794202c5b84570a9866f6b584b4
tuned signature -- prefer Isabelle/ML structure Integer;

diff -r 05e2cab9af8b -r b51515722274 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Fri Jan 01 17:08:51 2021 +0100
+++ b/src/HOL/Tools/numeral.ML	Fri Jan 01 17:35:04 2021 +0100
@@ -23,7 +23,7 @@
 
 fun mk_num_syntax n =
   if n > 0 then
-    (case IntInf.quotRem (n, 2) of
+    (case Integer.quot_rem n 2 of
       (0, 1) => Syntax.const \<^const_syntax>\<open>One\<close>
     | (n, 0) => Syntax.const \<^const_syntax>\<open>Bit0\<close> $ mk_num_syntax n
     | (n, 1) => Syntax.const \<^const_syntax>\<open>Bit1\<close> $ mk_num_syntax n)
diff -r 05e2cab9af8b -r b51515722274 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Fri Jan 01 17:08:51 2021 +0100
+++ b/src/Pure/General/integer.ML	Fri Jan 01 17:35:04 2021 +0100
@@ -14,6 +14,7 @@
   val prod: int list -> int
   val sign: int -> order
   val div_mod: int -> int -> int * int
+  val quot_rem: int -> int -> int * int
   val square: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
   val log2: int -> int
@@ -40,6 +41,7 @@
 fun sign x = int_ord (x, 0);
 
 fun div_mod x y = IntInf.divMod (x, y);
+fun quot_rem x y = IntInf.quotRem (x, y);
 
 fun square x = x * x;