src/HOL/hologic.ML

   val zero: term
   val is_zero: term -> bool
   val mk_Suc: term -> term
   val dest_Suc: term -> term
   val Suc_zero: term
-  val mk_nat: IntInf.int -> term
-  val dest_nat: term -> IntInf.int
+  val mk_nat: integer -> term
+  val dest_nat: term -> integer
   val class_size: string
   val size_const: typ -> term
   val bitT: typ
   val B0_const: term
   val B1_const: term

   val dest_bit: term -> int
   val intT: typ
   val pls_const: term
   val min_const: term
   val bit_const: term
-  val mk_numeral: IntInf.int -> term
-  val dest_numeral: term -> IntInf.int
+  val mk_numeral: integer -> term
+  val dest_numeral: term -> integer
   val number_of_const: typ -> term
   val add_numerals_of: term -> (term * typ) list -> (term * typ) list
-  val mk_number: typ -> IntInf.int -> term
-  val dest_number: term -> typ * IntInf.int
+  val mk_number: typ -> integer -> term
+  val dest_number: term -> typ * integer
   val realT: typ
   val nibbleT: typ
   val mk_nibble: int -> term
   val dest_nibble: term -> int
   val charT: typ

 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
 
 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
 
-val class_eq = "Code_Generator.eq";
+val class_eq = "HOL.eq";
 
 fun mk_mem (x, A) =
   let val setT = fastype_of A in
     Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
   end;

 val Suc_zero = mk_Suc zero;
 
 fun mk_nat n =
   let
     fun mk 0 = zero
-      | mk n = mk_Suc (mk (IntInf.- (n, 1)));
-  in if IntInf.< (n, 0)
+      | mk n = mk_Suc (mk (n -% 1));
+  in if n < 0
     then error "mk_nat: negative numeral"
     else mk n
   end;
 
-fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
-  | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1)
+fun dest_nat (Const ("HOL.zero_class.zero", _)) = Integer.zero
+  | dest_nat (Const ("Suc", _) $ t) = Integer.inc (dest_nat t)
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 val class_size = "Nat.size";
 
 fun size_const T = Const ("Nat.size_class.size", T --> natT);

 
 val intT = Type ("IntDef.int", []);
 
 val pls_const = Const ("Numeral.Pls", intT)
 and min_const = Const ("Numeral.Min", intT)
-and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
+and bit_const = Const ("Numeral.Bit", intT --> bitT --> intT);
 
 fun mk_numeral 0 = pls_const
   | mk_numeral ~1 = min_const
   | mk_numeral i =
-      let val (q, r) = IntInf.divMod (i, 2)
-      in bit_const $ mk_numeral q $ mk_bit (IntInf.toInt r) end;
+      let val (q, r) = Integer.divmod i 2
+      in bit_const $ mk_numeral q $ mk_bit (Integer.machine_int r) end;
 
 fun dest_numeral (Const ("Numeral.Pls", _)) = 0
   | dest_numeral (Const ("Numeral.Min", _)) = ~1
   | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
-      2 * dest_numeral bs + IntInf.fromInt (dest_bit b)
+      2 *% dest_numeral bs +% Integer.int (dest_bit b)
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
 fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
 
 fun add_numerals_of (Const _) =