# HG changeset patch
# User paulson
# Date 1146132716 -7200
# Node ID a6205c6203ea3445841afa1e9fca0df829d5da3c
# Parent  868cf5051ff568c91c4df992ca9baec513b91d23
renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum

diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/Integ/cooper_dec.ML
--- 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*)	  
 	  
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/Integ/int_arith1.ML
--- 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
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/Integ/nat_simprocs.ML
--- 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
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/Library/EfficientNat.thy
--- 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;
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/Tools/Presburger/cooper_dec.ML
--- 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*)	  
 	  
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/Tools/numeral_syntax.ML
--- 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) =
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/arith_data.ML
--- 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;
 
diff -r 868cf5051ff5 -r a6205c6203ea src/HOL/hologic.ML
--- 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 *)