# HG changeset patch
# User haftmann
# Date 1181049368 -7200
# Node ID b99dce43d252853acb9f91ddb8d100ed62390d39
# Parent  309a57cae0125d231c23c7e73878f45a0040774e
merged Code_Generator.thy into HOL.thy

diff -r 309a57cae012 -r b99dce43d252 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Tue Jun 05 12:12:25 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(*  ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Setup of code generator tools *}
-
-theory Code_Generator
-imports HOL
-uses "~~/src/HOL/Tools/recfun_codegen.ML"
-begin
-
-ML {*
-structure HOL =
-struct
-  val thy = theory "HOL";
-end;
-*}  -- "belongs to theory HOL"
-
-subsection {* SML code generator setup *}
-
-types_code
-  "bool"  ("bool")
-attach (term_of) {*
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-*}
-attach (test) {*
-fun gen_bool i = one_of [false, true];
-*}
-  "prop"  ("bool")
-attach (term_of) {*
-fun term_of_prop b =
-  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
-*}
-
-consts_code
-  "Trueprop" ("(_)")
-  "True"    ("true")
-  "False"   ("false")
-  "Not"     ("Bool.not")
-  "op |"    ("(_ orelse/ _)")
-  "op &"    ("(_ andalso/ _)")
-  "If"      ("(if _/ then _/ else _)")
-
-setup {*
-let
-
-fun eq_codegen thy defs gr dep thyname b t =
-    (case strip_comb t of
-       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
-     | (Const ("op =", _), [t, u]) =>
-          let
-            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
-            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
-            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
-          in
-            SOME (gr''', Codegen.parens
-              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
-          end
-     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
-         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
-     | _ => NONE);
-
-in
-
-Codegen.add_codegen "eq_codegen" eq_codegen
-#> RecfunCodegen.setup
-
-end
-*}
-
-text {* Evaluation *}
-
-method_setup evaluation = {*
-let
-
-fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
-  (Conv.goals_conv (equal i) Codegen.evaluation_conv));
-
-in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
-*} "solve goal by evaluation"
-
-
-subsection {* Generic code generator setup *}
-
-text {* operational equality for code generation *}
-
-class eq (attach "op =") = type
-
-
-text {* using built-in Haskell equality *}
-
-code_class eq
-  (Haskell "Eq" where "op =" \<equiv> "(==)")
-
-code_const "op ="
-  (Haskell infixl 4 "==")
-
-
-text {* type bool *}
-
-code_datatype True False
-
-lemma [code func]:
-  shows "(False \<and> x) = False"
-    and "(True \<and> x) = x"
-    and "(x \<and> False) = False"
-    and "(x \<and> True) = x" by simp_all
-
-lemma [code func]:
-  shows "(False \<or> x) = x"
-    and "(True \<or> x) = True"
-    and "(x \<or> False) = x"
-    and "(x \<or> True) = True" by simp_all
-
-lemma [code func]:
-  shows "(\<not> True) = False"
-    and "(\<not> False) = True" by (rule HOL.simp_thms)+
-
-lemmas [code] = imp_conv_disj
-
-lemmas [code func] = if_True if_False
-
-instance bool :: eq ..
-
-lemma [code func]:
-  shows "True = P \<longleftrightarrow> P"
-    and "False = P \<longleftrightarrow> \<not> P"
-    and "P = True \<longleftrightarrow> P"
-    and "P = False \<longleftrightarrow> \<not> P" by simp_all
-
-code_type bool
-  (SML "bool")
-  (OCaml "bool")
-  (Haskell "Bool")
-
-code_instance bool :: eq
-  (Haskell -)
-
-code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
-
-code_const True and False and Not and "op &" and "op |" and If
-  (SML "true" and "false" and "not"
-    and infixl 1 "andalso" and infixl 0 "orelse"
-    and "!(if (_)/ then (_)/ else (_))")
-  (OCaml "true" and "false" and "not"
-    and infixl 4 "&&" and infixl 2 "||"
-    and "!(if (_)/ then (_)/ else (_))")
-  (Haskell "True" and "False" and "not"
-    and infixl 3 "&&" and infixl 2 "||"
-    and "!(if (_)/ then (_)/ else (_))")
-
-code_reserved SML
-  bool true false not
-
-code_reserved OCaml
-  bool true false not
-
-
-text {* type prop *}
-
-code_datatype Trueprop "prop"
-
-
-text {* type itself *}
-
-code_datatype "TYPE('a)"
-
-
-text {* code generation for undefined as exception *}
-
-code_const undefined
-  (SML "raise/ Fail/ \"undefined\"")
-  (OCaml "failwith/ \"undefined\"")
-  (Haskell "error/ \"undefined\"")
-
-code_reserved SML Fail
-code_reserved OCaml failwith
-
-
-subsection {* Evaluation oracle *}
-
-oracle eval_oracle ("term") = {* fn thy => fn t => 
-  if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
-  then t
-  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
-*}
-
-method_setup eval = {*
-let
-  fun eval_tac thy = 
-    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
-in 
-  Method.ctxt_args (fn ctxt => 
-    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
-end
-*} "solve goal by evaluation"
-
-
-subsection {* Normalization by evaluation *}
-
-method_setup normalization = {*
-let
-  fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
-    (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
-      NBE.normalization_conv)));
-in
-  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
-end
-*} "solve goal by normalization"
-
-
-text {* lazy @{const If} *}
-
-definition
-  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  [code func del]: "if_delayed b f g = (if b then f True else g False)"
-
-lemma [code func]:
-  shows "if_delayed True f g = f True"
-    and "if_delayed False f g = g False"
-  unfolding if_delayed_def by simp_all
-
-lemma [normal pre, symmetric, normal post]:
-  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
-  unfolding if_delayed_def ..
-
-hide (open) const if_delayed
-
-end
diff -r 309a57cae012 -r b99dce43d252 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 05 15:16:08 2007 +0200
@@ -8,6 +8,7 @@
 theory HOL
 imports CPure
 uses
+  "~~/src/Tools/integer.ML"
   "hologic.ML"
   "~~/src/Provers/splitter.ML"
   "~~/src/Provers/hypsubst.ML"
@@ -20,8 +21,7 @@
   "~~/src/Provers/classical.ML"
   "~~/src/Provers/blast.ML"
   "~~/src/Provers/clasimp.ML"
-  "~~/src/Pure/General/int.ML"
-  "~~/src/Pure/General/rat.ML"
+  "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/fast_lin_arith.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"
   "~~/src/Provers/quantifier1.ML"
@@ -33,6 +33,7 @@
   "~~/src/Provers/quasi.ML"
   "~~/src/Provers/order.ML"
   ("simpdata.ML")
+  ("~~/src/HOL/Tools/recfun_codegen.ML")
   "Tools/res_atpset.ML"
 begin
 
@@ -1495,6 +1496,222 @@
 *}
 
 
+subsection {* Code generator setup *}
+
+subsubsection {* SML code generator setup *}
+
+use "~~/src/HOL/Tools/recfun_codegen.ML"
+
+types_code
+  "bool"  ("bool")
+attach (term_of) {*
+fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
+*}
+attach (test) {*
+fun gen_bool i = one_of [false, true];
+*}
+  "prop"  ("bool")
+attach (term_of) {*
+fun term_of_prop b =
+  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
+*}
+
+consts_code
+  "Trueprop" ("(_)")
+  "True"    ("true")
+  "False"   ("false")
+  "Not"     ("Bool.not")
+  "op |"    ("(_ orelse/ _)")
+  "op &"    ("(_ andalso/ _)")
+  "If"      ("(if _/ then _/ else _)")
+
+setup {*
+let
+
+fun eq_codegen thy defs gr dep thyname b t =
+    (case strip_comb t of
+       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
+     | (Const ("op =", _), [t, u]) =>
+          let
+            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
+            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
+            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
+          in
+            SOME (gr''', Codegen.parens
+              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
+          end
+     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
+         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
+     | _ => NONE);
+
+in
+
+Codegen.add_codegen "eq_codegen" eq_codegen
+#> RecfunCodegen.setup
+
+end
+*}
+
+text {* Evaluation *}
+
+method_setup evaluation = {*
+let
+
+fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
+  (Conv.goals_conv (equal i) Codegen.evaluation_conv));
+
+in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
+*} "solve goal by evaluation"
+
+
+subsubsection {* Generic code generator setup *}
+
+text {* operational equality for code generation *}
+
+class eq (attach "op =") = type
+
+
+text {* using built-in Haskell equality *}
+
+code_class eq
+  (Haskell "Eq" where "op =" \<equiv> "(==)")
+
+code_const "op ="
+  (Haskell infixl 4 "==")
+
+
+text {* type bool *}
+
+code_datatype True False
+
+lemma [code func]:
+  shows "(False \<and> x) = False"
+    and "(True \<and> x) = x"
+    and "(x \<and> False) = False"
+    and "(x \<and> True) = x" by simp_all
+
+lemma [code func]:
+  shows "(False \<or> x) = x"
+    and "(True \<or> x) = True"
+    and "(x \<or> False) = x"
+    and "(x \<or> True) = True" by simp_all
+
+lemma [code func]:
+  shows "(\<not> True) = False"
+    and "(\<not> False) = True" by (rule HOL.simp_thms)+
+
+lemmas [code] = imp_conv_disj
+
+lemmas [code func] = if_True if_False
+
+instance bool :: eq ..
+
+lemma [code func]:
+  shows "True = P \<longleftrightarrow> P"
+    and "False = P \<longleftrightarrow> \<not> P"
+    and "P = True \<longleftrightarrow> P"
+    and "P = False \<longleftrightarrow> \<not> P" by simp_all
+
+code_type bool
+  (SML "bool")
+  (OCaml "bool")
+  (Haskell "Bool")
+
+code_instance bool :: eq
+  (Haskell -)
+
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const True and False and Not and "op &" and "op |" and If
+  (SML "true" and "false" and "not"
+    and infixl 1 "andalso" and infixl 0 "orelse"
+    and "!(if (_)/ then (_)/ else (_))")
+  (OCaml "true" and "false" and "not"
+    and infixl 4 "&&" and infixl 2 "||"
+    and "!(if (_)/ then (_)/ else (_))")
+  (Haskell "True" and "False" and "not"
+    and infixl 3 "&&" and infixl 2 "||"
+    and "!(if (_)/ then (_)/ else (_))")
+
+code_reserved SML
+  bool true false not
+
+code_reserved OCaml
+  bool true false not
+
+
+text {* type prop *}
+
+code_datatype Trueprop "prop"
+
+
+text {* type itself *}
+
+code_datatype "TYPE('a)"
+
+
+text {* code generation for undefined as exception *}
+
+code_const undefined
+  (SML "raise/ Fail/ \"undefined\"")
+  (OCaml "failwith/ \"undefined\"")
+  (Haskell "error/ \"undefined\"")
+
+code_reserved SML Fail
+code_reserved OCaml failwith
+
+
+subsubsection {* Evaluation oracle *}
+
+oracle eval_oracle ("term") = {* fn thy => fn t => 
+  if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
+  then t
+  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
+*}
+
+method_setup eval = {*
+let
+  fun eval_tac thy = 
+    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
+in 
+  Method.ctxt_args (fn ctxt => 
+    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
+end
+*} "solve goal by evaluation"
+
+
+subsubsection {* Normalization by evaluation *}
+
+method_setup normalization = {*
+let
+  fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
+    (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
+      NBE.normalization_conv)));
+in
+  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
+end
+*} "solve goal by normalization"
+
+
+text {* lazy @{const If} *}
+
+definition
+  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  [code func del]: "if_delayed b f g = (if b then f True else g False)"
+
+lemma [code func]:
+  shows "if_delayed True f g = f True"
+    and "if_delayed False f g = g False"
+  unfolding if_delayed_def by simp_all
+
+lemma [normal pre, symmetric, normal post]:
+  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
+  unfolding if_delayed_def ..
+
+hide (open) const if_delayed
+
+
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
diff -r 309a57cae012 -r b99dce43d252 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 05 15:16:08 2007 +0200
@@ -80,9 +80,9 @@
   $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML		\
   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
   $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
-  $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML			\
-  $(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.ML			\
-  ATP_Linkup.thy Accessible_Part.thy Code_Generator.thy Datatype.thy	\
+  $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML			\
+  $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML			\
+  ATP_Linkup.thy Accessible_Part.thy Datatype.thy	\
   Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy		\
   FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy		\
   Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy\
@@ -152,7 +152,7 @@
 
 HOL-Complex: HOL $(OUT)/HOL-Complex
 
-$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Pure/General/float.ML \
+$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
   Library/Zorn.thy							\
   Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/float_arith.ML	\
   Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy	\
diff -r 309a57cae012 -r b99dce43d252 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/Orderings.thy	Tue Jun 05 15:16:08 2007 +0200
@@ -6,7 +6,7 @@
 header {* Syntactic and abstract orders *}
 
 theory Orderings
-imports Code_Generator
+imports HOL
 begin
 
 subsection {* Order syntax *}
diff -r 309a57cae012 -r b99dce43d252 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/Product_Type.thy	Tue Jun 05 15:16:08 2007 +0200
@@ -7,7 +7,7 @@
 header {* Cartesian products *}
 
 theory Product_Type
-imports Typedef Fun Code_Generator
+imports Typedef Fun
 uses ("Tools/split_rule.ML")
 begin
 
diff -r 309a57cae012 -r b99dce43d252 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/Typedef.thy	Tue Jun 05 15:16:08 2007 +0200
@@ -13,14 +13,19 @@
   ("Tools/typedef_codegen.ML")
 begin
 
+ML {*
+structure HOL = struct val thy = theory "HOL" end;
+*}  -- "belongs to theory HOL"
+
 locale type_definition =
   fixes Rep and Abs and A
   assumes Rep: "Rep x \<in> A"
     and Rep_inverse: "Abs (Rep x) = x"
     and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
   -- {* This will be axiomatized for each typedef! *}
+begin
 
-lemma (in type_definition) Rep_inject:
+lemma Rep_inject:
   "(Rep x = Rep y) = (x = y)"
 proof
   assume "Rep x = Rep y"
@@ -33,7 +38,7 @@
   thus "Rep x = Rep y" by (simp only:)
 qed
 
-lemma (in type_definition) Abs_inject:
+lemma Abs_inject:
   assumes x: "x \<in> A" and y: "y \<in> A"
   shows "(Abs x = Abs y) = (x = y)"
 proof
@@ -47,7 +52,7 @@
   thus "Abs x = Abs y" by (simp only:)
 qed
 
-lemma (in type_definition) Rep_cases [cases set]:
+lemma Rep_cases [cases set]:
   assumes y: "y \<in> A"
     and hyp: "!!x. y = Rep x ==> P"
   shows P
@@ -56,7 +61,7 @@
   thus "y = Rep (Abs y)" ..
 qed
 
-lemma (in type_definition) Abs_cases [cases type]:
+lemma Abs_cases [cases type]:
   assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
   shows P
 proof (rule r)
@@ -65,7 +70,7 @@
   show "Rep x \<in> A" by (rule Rep)
 qed
 
-lemma (in type_definition) Rep_induct [induct set]:
+lemma Rep_induct [induct set]:
   assumes y: "y \<in> A"
     and hyp: "!!x. P (Rep x)"
   shows "P y"
@@ -75,7 +80,7 @@
   finally show "P y" .
 qed
 
-lemma (in type_definition) Abs_induct [induct type]:
+lemma Abs_induct [induct type]:
   assumes r: "!!y. y \<in> A ==> P (Abs y)"
   shows "P x"
 proof -
@@ -85,6 +90,8 @@
   finally show "P x" .
 qed
 
+end
+
 use "Tools/typedef_package.ML"
 use "Tools/typecopy_package.ML"
 use "Tools/typedef_codegen.ML"
diff -r 309a57cae012 -r b99dce43d252 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/hologic.ML	Tue Jun 05 15:16:08 2007 +0200
@@ -71,8 +71,8 @@
   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
@@ -84,12 +84,12 @@
   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
@@ -186,7 +186,7 @@
 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
@@ -298,14 +298,14 @@
 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";
@@ -335,18 +335,18 @@
 
 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);