--- a/src/HOL/Integ/cooper_dec.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Thu Apr 27 12:11:56 2006 +0200
@@ -80,7 +80,7 @@
fun mk_numeral 0 = Const("0",HOLogic.intT)
|mk_numeral 1 = Const("1",HOLogic.intT)
- |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n);
+ |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n);
(*Transform an Term to an natural number*)
--- a/src/HOL/Integ/int_arith1.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu Apr 27 12:11:56 2006 +0200
@@ -182,7 +182,7 @@
(** Utilities **)
-fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_bin n;
+fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n;
(*Decodes a binary INTEGER*)
fun dest_numeral (Const("0", _)) = 0
--- a/src/HOL/Integ/nat_simprocs.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Apr 27 12:11:56 2006 +0200
@@ -23,7 +23,7 @@
(*Utilities*)
-fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n;
+fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_binum n;
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
fun dest_numeral (Const ("0", _)) = 0
--- a/src/HOL/Library/EfficientNat.thy Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Thu Apr 27 12:11:56 2006 +0200
@@ -36,7 +36,7 @@
fun term_of_nat 0 = Const ("0", HOLogic.natT)
| term_of_nat 1 = Const ("1", HOLogic.natT)
| term_of_nat i = HOLogic.number_of_const HOLogic.natT $
- HOLogic.mk_bin (IntInf.fromInt i);
+ HOLogic.mk_binum (IntInf.fromInt i);
*}
attach (test) {*
fun gen_nat i = random_range 0 i;
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Thu Apr 27 12:11:56 2006 +0200
@@ -80,7 +80,7 @@
fun mk_numeral 0 = Const("0",HOLogic.intT)
|mk_numeral 1 = Const("1",HOLogic.intT)
- |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n);
+ |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n);
(*Transform an Term to an natural number*)
--- a/src/HOL/Tools/numeral_syntax.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Thu Apr 27 12:11:56 2006 +0200
@@ -38,7 +38,7 @@
(* translation of integer numeral tokens to and from bitstrings *)
fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
- (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str))))
+ (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (valOf (IntInf.fromString str))))
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
--- a/src/HOL/arith_data.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/arith_data.ML Thu Apr 27 12:11:56 2006 +0200
@@ -367,7 +367,7 @@
let val {discrete, inj_consts, ...} = ArithTheoryData.get sg
in decomp2 (sg,discrete,inj_consts) end
-fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
+fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n)
end;
--- a/src/HOL/hologic.ML Thu Apr 27 12:11:05 2006 +0200
+++ b/src/HOL/hologic.ML Thu Apr 27 12:11:56 2006 +0200
@@ -83,7 +83,7 @@
val number_of_const: typ -> term
val int_of: int list -> IntInf.int
val dest_binum: term -> IntInf.int
- val mk_bin: IntInf.int -> term
+ val mk_binum: IntInf.int -> term
val bin_of : term -> int list
val listT : typ -> typ
val mk_list: ('a -> term) -> typ -> 'a list -> term
@@ -318,7 +318,7 @@
| mk_bit 1 = B1_const
| mk_bit _ = sys_error "mk_bit";
-fun mk_bin n =
+fun mk_binum n =
let
fun mk_bit n = if n = 0 then B0_const else B1_const;
@@ -341,7 +341,7 @@
fun mk_int 0 = Const ("0", intT)
| mk_int 1 = Const ("1", intT)
- | mk_int i = number_of_const intT $ mk_bin i;
+ | mk_int i = number_of_const intT $ mk_binum i;
(* real *)