# HG changeset patch
# User haftmann
# Date 1166021131 -3600
# Node ID 2f2b6a965ccc8414c270972cae32bf45134ed26f
# Parent  8eb82ffcdd15998ab6a84b04f9197d92a5f0aa45
introduced mk/dest_numeral/number for mk/dest_binum etc.

diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/IntArith.thy	Wed Dec 13 15:45:31 2006 +0100
@@ -16,15 +16,9 @@
 
 subsection{*Instantiating Binary Arithmetic for the Integers*}
 
-instance
-  int :: number ..
-
-defs (overloaded)
-  int_number_of_def: "(number_of w :: int) == of_int w"
-    --{*the type constraint is essential!*}
-
 instance int :: number_ring
-by (intro_classes, simp add: int_number_of_def) 
+  int_number_of_def: "number_of w \<equiv> of_int w"
+  by intro_classes (simp only: int_number_of_def)
 
 
 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
@@ -400,17 +394,6 @@
 
 declare int_code_rewrites [code func]
 
-ML {*
-structure Numeral =
-struct
- 
-fun int_of_numeral thy num = HOLogic.dest_binum num
-  handle TERM _
-    => error ("not a number: " ^ Sign.string_of_term thy num);
- 
-end;
-*}
-
 code_type bit
   (SML "bool")
   (Haskell "Bool")
@@ -435,7 +418,7 @@
      and "(-)/ _/ 1")
 
 setup {*
-  CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral Numeral.int_of_numeral)
+  CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral (try HOLogic.dest_numeral))
 *}
 
 
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Wed Dec 13 15:45:31 2006 +0100
@@ -863,7 +863,7 @@
 types_code
   "int" ("int")
 attach (term_of) {*
-val term_of_int = HOLogic.mk_int o IntInf.fromInt;
+val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
 *}
 attach (test) {*
 fun gen_int i = one_of [~1, 1] * random_range 0 i;
@@ -955,15 +955,15 @@
   IntDef Integer
 
 ML {*
-fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
-      Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
+fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
+      if T = HOLogic.intT then
         (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
-           Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE)
-  | number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of",
-      Type ("fun", [_, Type ("nat", [])])) $ bin) =
-        SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
+          (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
+      else if T = HOLogic.natT then
+        SOME (Codegen.invoke_codegen thy defs dep module b (gr,
           Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ bin)))
+            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
+      else NONE
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}
 
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/Numeral.thy	Wed Dec 13 15:45:31 2006 +0100
@@ -31,20 +31,19 @@
 datatype bit = B0 | B1
 
 definition
-  Pls :: int where "Pls == 0"
+  Pls :: int where
+  "Pls = 0"
 
 definition
-  Min :: int where "Min == - 1"
+  Min :: int where
+  "Min = - 1"
 
 definition
   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
-  "k BIT b == (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
 
-axclass
-  number < type  -- {* for numeric types: nat, int, real, \dots *}
-
-consts
-  number_of :: "int \<Rightarrow> 'a::number"
+class number = -- {* for numeric types: nat, int, real, \dots *}
+  fixes number_of :: "int \<Rightarrow> 'a"
 
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -11,8 +11,8 @@
 sig
   exception COOPER
   val is_arith_rel : term -> bool
-  val mk_numeral : IntInf.int -> term
-  val dest_numeral : term -> IntInf.int
+  val mk_number : IntInf.int -> term
+  val dest_number : term -> IntInf.int
   val is_numeral : term -> bool
   val zero : term
   val one : term
@@ -76,32 +76,32 @@
  
 (*Transform a natural number to a term*) 
  
-fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
-   |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); 
+fun mk_number 0 = Const("HOL.zero",HOLogic.intT)
+   |mk_number 1 = Const("HOL.one",HOLogic.intT)
+   |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n); 
  
 (*Transform an Term to an natural number*)	  
 	  
-fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
-   |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
-   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
-       HOLogic.dest_binum n;
+fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0
+   |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1
+   |dest_number (Const ("Numeral.number_of",_) $ n) = 
+       HOLogic.dest_numeral n;
 (*Some terms often used for pattern matching*) 
  
-val zero = mk_numeral 0; 
-val one = mk_numeral 1; 
+val zero = mk_number 0; 
+val one = mk_number 1; 
  
 (*Tests if a Term is representing a number*) 
  
-fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_numeral t); 
+fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t); 
  
 (*maps a unary natural function on a term containing an natural number*) 
  
-fun numeral1 f n = mk_numeral (f(dest_numeral n)); 
+fun numeral1 f n = mk_number (f(dest_number n)); 
  
 (*maps a binary natural function on 2 term containing  natural numbers*) 
  
-fun numeral2 f m n = mk_numeral(f(dest_numeral m) (dest_numeral n)); 
+fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n)); 
  
 (* ------------------------------------------------------------------------- *) 
 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k          *) 
@@ -178,9 +178,9 @@
  Free(x,T)*) 
   
 fun lint vars tm = if is_numeral tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) 
+   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero)) 
   |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
+  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
   |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
   |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
   |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
@@ -188,8 +188,8 @@
         let val s' = lint vars s  
             val t' = lint vars t  
         in 
-        if is_numeral s' then (linear_cmul (dest_numeral s') t') 
-        else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
+        if is_numeral s' then (linear_cmul (dest_number s') t') 
+        else if is_numeral t' then (linear_cmul (dest_number t') s') 
  
          else raise COOPER
          end 
@@ -205,7 +205,7 @@
  
 fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
     if is_numeral c then   
-      let val c' = (mk_numeral(abs(dest_numeral c)))  
+      let val c' = (mk_number(abs(dest_number c)))  
       in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
@@ -214,11 +214,11 @@
   |linform vars  (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   |linform vars  (Const("Orderings.less_eq",_)$ s $ t ) = 
-        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
+        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
   |linform vars  (Const("op >=",_)$ s $ t ) = 
         (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
 	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $s $(mk_numeral 1)) $ t)) 
+	HOLogic.intT) $s $(mk_number 1)) $ t)) 
  
    |linform vars  fm =  fm; 
  
@@ -228,7 +228,7 @@
  
 fun posineq fm = case fm of  
  (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
-   (HOLogic.mk_binrel "Orderings.less"  (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) ))) 
+   (HOLogic.mk_binrel "Orderings.less"  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
   | ( Const ("op &",_) $ p $ q)  => HOLogic.mk_conj (posineq p,posineq q)
   | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
   | _ => fm; 
@@ -245,7 +245,7 @@
  
 fun formlcm x fm = case fm of 
     (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
-    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
+    (is_arith_rel fm) andalso (x = y) then  (abs(dest_number c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
   | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
@@ -259,9 +259,9 @@
      case fm of  
       (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_numeral c) 
+        let val m = l div (dest_number c) 
             val n = (if p = "Orderings.less" then abs(m) else m) 
-            val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) 
+            val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x) 
 	in
         (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	end 
@@ -281,9 +281,9 @@
       if l = 1 then fm' 
 	 else 
      let val xp = (HOLogic.mk_binop "HOL.plus"  
-     		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
+     		((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
 	in 
-      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
+      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) 
       end 
   end; 
  
@@ -294,9 +294,9 @@
     case fm of  
       (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_numeral c) 
+        let val m = l div (dest_number c) 
             val n = (if p = "Orderings.less" then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
             in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	    end 
 	else fm 
@@ -320,7 +320,7 @@
   |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
-	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
+	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
 	          else error "minusinf : term not in normal form!!!"
 	else fm
 	 
@@ -341,7 +341,7 @@
   |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
-	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
 	     else error "plusinf : term not in normal form!!!"
 	else fm 
 
@@ -355,7 +355,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
-        if x = y then abs(dest_numeral d) else 1 
+        if x = y then abs(dest_number d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
   |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) 
@@ -375,7 +375,7 @@
    	  |_ =>[]) 
 			 
 			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
   |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
   |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
   |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
@@ -395,8 +395,8 @@
    	  |_ =>[])
 
 			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
-  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
+  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
   |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
   |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
   |_ => [];
@@ -410,7 +410,7 @@
    ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
       if (x = y) andalso (is_arith_rel fm)  
       then  
-        let val ct = linear_cmul (dest_numeral c) t  
+        let val ct = linear_cmul (dest_number c) t  
 	in (HOLogic.mk_binrel p (d, linear_add vars ct z)) 
 	end 
 	else fm 
@@ -430,16 +430,16 @@
 fun dvd_op (d, t) = 
  if not(is_numeral d) then raise DVD_UNKNOWN
  else let 
-   val dn = dest_numeral d
+   val dn = dest_number d
    fun coeffs_of x = case x of 
      Const(p,_) $ tl $ tr => 
        if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
           else if p = "HOL.times" 
 	        then if (is_numeral tr) 
-		 then [(dest_numeral tr) * (dest_numeral tl)] 
-		 else [dest_numeral tl]
+		 then [(dest_number tr) * (dest_number tl)] 
+		 else [dest_number tl]
 	        else []
-    |_ => if (is_numeral t) then [dest_numeral t]  else []
+    |_ => if (is_numeral t) then [dest_number t]  else []
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
@@ -466,12 +466,12 @@
       handle _ => at)
     else
   case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
+    SOME f => ((if (f ((dest_number s),(dest_number t))) then 
     HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
       | _ =>  at) 
@@ -482,13 +482,13 @@
 fun evalc_atom at = case at of  
   (Const (p,_) $ s $ t) =>
    ( case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
+    SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const 
                 else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
+    SOME f => ((if (f ((dest_number s),(dest_number t))) 
                then HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
       | _ =>  at) 
@@ -659,8 +659,8 @@
     |mk_uni_vars T (Free (v,_)) = Free (v,T) 
     |mk_uni_vars T tm = tm; 
  
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2)) 
-    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2)) 
+fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2)) 
+    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2)) 
     |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
     |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
     |mk_uni_int T tm = tm; 
@@ -680,8 +680,8 @@
     val p_inf = simpl (minusinf x p) 
     val bset = bset x p 
     val js = myupto 1 (divlcm x p)
-    fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p  
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)  
+    fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p  
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset)  
    in (list_disj (map stage js))
     end 
   | _ => error "cooper: not an existential formula"; 
@@ -699,8 +699,8 @@
     val p_inf = simpl (plusinf x p)
     val aset = aset x p
     val js = myupto 1 (divlcm x p)
-    fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
+    fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset)
    in (list_disj (map stage js))
    end
   | _ => error "cooper: not an existential formula";
@@ -711,13 +711,13 @@
 fun inf_w mi d vars x p = 
   let val f = if mi then minusinf else plusinf in
    case (simpl (minusinf x p)) of
-   Const("True",_)  => (SOME (mk_numeral 1), HOLogic.true_const)
+   Const("True",_)  => (SOME (mk_number 1), HOLogic.true_const)
   |Const("False",_) => (NONE,HOLogic.false_const)
   |F => 
       let 
       fun h n =
-       case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of 
-	Const("True",_) => (SOME (mk_numeral n),HOLogic.true_const)
+       case ((simpl o evalc) (linrep vars x (mk_number n) F)) of 
+	Const("True",_) => (SOME (mk_number n),HOLogic.true_const)
        |F' => if n=1 then (NONE,F')
 	     else let val (rw,rf) = h (n-1) in 
 	       (rw,HOLogic.mk_disj(F',rf))
@@ -736,7 +736,7 @@
              in (rw,HOLogic.mk_disj(F',rf)) 
 	     end)
     val f = if b then linear_add else linear_sub
-    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
+    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) []
     in h p_elements
     end;
 
@@ -769,8 +769,8 @@
     if (length bst) <= (length ast) 
      then (simpl (minusinf x p),linear_add,bst)
      else (simpl (plusinf x p), linear_sub,ast)
-    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+    fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
     fun stageh n = ((if n = 0 then []
 	else 
 	let 
@@ -805,8 +805,8 @@
      then (true,bst)
      else (false,ast)
     in withness d p_inf S vars x p 
-(*    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+(*    fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
    in (list_disj (map stage js))
 *)
    end
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/cooper_proof.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -33,7 +33,7 @@
 val presburger_ss = simpset ()
   addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
 
-val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
+val cboolT = ctyp_of HOL.thy HOLogic.boolT;
 
 (*Theorems that will be used later for the proofgeneration*)
 
@@ -163,7 +163,7 @@
 fun norm_zero_one fm = case fm of
   (Const ("HOL.times",_) $ c $ t) => 
     if c = one then (norm_zero_one t)
-    else if (dest_numeral c = ~1) 
+    else if (dest_number c = ~1) 
          then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
          else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
@@ -253,18 +253,18 @@
 fun decomp_adjustcoeffeq sg x l fm = case fm of
     (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
      let  
-        val m = l div (dest_numeral c) 
+        val m = l div (dest_number c) 
         val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) 
+        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x)) 
         val rs = if (x = y) 
-                 then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
+                 then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
                  else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
-        val ck = cterm_of sg (mk_numeral n)
+        val ck = cterm_of sg (mk_number n)
         val cc = cterm_of sg c
         val ct = cterm_of sg z
         val cx = cterm_of sg y
         val pre = prove_elementar sg "lf" 
-            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral n)))
+            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
         val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
         end
@@ -273,12 +273,12 @@
       c $ y ) $t )) => 
    if (is_arith_rel fm) andalso (x = y) 
    then  
-        let val m = l div (dest_numeral c) 
+        let val m = l div (dest_number c) 
            val k = (if p = "Orderings.less" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
+           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
            val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
 
-           val ck = cterm_of sg (mk_numeral k)
+           val ck = cterm_of sg (mk_number k)
            val cc = cterm_of sg c
            val ct = cterm_of sg t
            val cx = cterm_of sg x
@@ -288,21 +288,21 @@
 	case p of
 	  "Orderings.less" => 
 	let val pre = prove_elementar sg "lf" 
-	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral k)))
+	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
             val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
 	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
          end
 
            |"op =" =>
 	     let val pre = prove_elementar sg "lf" 
-	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
 	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
              end
 
              |"Divides.dvd" =>
 	       let val pre = prove_elementar sg "lf" 
-	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
                    val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
                in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
                         
@@ -574,7 +574,7 @@
 
    |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
-	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
+	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
 	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
 	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
@@ -675,7 +675,7 @@
 
    |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
-        if pm1 = (mk_numeral ~1) then 
+        if pm1 = (mk_number ~1) then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
               val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
 	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
@@ -734,7 +734,7 @@
     (Const (p,_) $ s $ t) =>(  
     case AList.lookup (op =) operations p of 
         SOME f => 
-           ((if (f ((dest_numeral s),(dest_numeral t))) 
+           ((if (f ((dest_number s),(dest_number t))) 
              then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
              else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
 		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
@@ -742,7 +742,7 @@
      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
        case AList.lookup (op =) operations p of 
          SOME f => 
-           ((if (f ((dest_numeral s),(dest_numeral t))) 
+           ((if (f ((dest_number s),(dest_number t))) 
              then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
              else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
 		      handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) 
@@ -842,14 +842,14 @@
    val ss = presburger_ss addsimps
      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
-   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
    (* e_ac_thm : Ex x. efm = EX x. fm*)
    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    (* A and B set of the formula*)
    val A = aset x cfm
    val B = bset x cfm
    (* the divlcm (delta) of the formula*)
-   val dlcm = mk_numeral (divlcm x cfm)
+   val dlcm = mk_number (divlcm x cfm)
    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    val cms = if ((length A) < (length B )) then "pi" else "mi"
 (*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
@@ -906,7 +906,7 @@
    val ss = presburger_ss addsimps
      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
-   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
    (* e_ac_thm : Ex x. efm = EX x. fm*)
    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
@@ -923,7 +923,7 @@
     val A = aset x cfm
     val B = bset x cfm
     (* the divlcm (delta) of the formula*)
-    val dlcm = mk_numeral (divlcm x cfm)
+    val dlcm = mk_number (divlcm x cfm)
     (* Which set is smaller to generate the (hoepfully) shorter proof*)
     val cms = if ((length A) < (length B )) then "pi" else "mi"
     (* synthesize the proof of cooper's theorem*)
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -160,7 +160,7 @@
       (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   | numterm_ord
      (Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
-     num_ord (HOLogic.dest_binum v, HOLogic.dest_binum w)
+     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
   | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
   | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
   | numterm_ord (t, u) =
@@ -181,18 +181,18 @@
 
 (** Utilities **)
 
-fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n;
+fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
 
 (*Decodes a binary INTEGER*)
-fun dest_numeral (Const("HOL.zero", _)) = 0
-  | dest_numeral (Const("HOL.one", _)) = 1
-  | dest_numeral (Const("Numeral.number_of", _) $ w) =
-     (HOLogic.dest_binum w
-      handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+fun dest_number (Const("HOL.zero", _)) = 0
+  | dest_number (Const("HOL.one", _)) = 1
+  | dest_number (Const("Numeral.number_of", _) $ w) =
+     (HOLogic.dest_numeral w
+      handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_number:1", [w]))
+  | dest_number t = raise TERM("Int_Numeral_Simprocs.dest_number:2", [t]);
 
 fun find_first_numeral past (t::terms) =
-        ((dest_numeral t, rev past @ terms)
+        ((dest_number t, rev past @ terms)
          handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
@@ -204,12 +204,12 @@
   end;
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
-fun mk_sum T []        = mk_numeral T 0
+fun mk_sum T []        = mk_number T 0
   | mk_sum T [t,u]     = mk_plus (t, u)
   | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
 
 (*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum T []        = mk_numeral T 0
+fun long_mk_sum T []        = mk_number T 0
   | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
 
 val dest_plus = HOLogic.dest_bin "HOL.plus" Term.dummyT;
@@ -230,14 +230,14 @@
 val mk_times = HOLogic.mk_binop "HOL.times";
 
 fun mk_prod T = 
-  let val one = mk_numeral T 1
+  let val one = mk_number T 1
   fun mk [] = one
     | mk [t] = t
     | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
   in mk end;
 
 (*This version ALWAYS includes a trailing one*)
-fun long_mk_prod T []        = mk_numeral T 1
+fun long_mk_prod T []        = mk_number T 1
   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
 
 val dest_times = HOLogic.dest_bin "HOL.times" Term.dummyT;
@@ -248,7 +248,7 @@
       handle TERM _ => [t];
 
 (*DON'T do the obvious simplifications; that would create special cases*)
-fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
+fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
 fun dest_coeff sign (Const ("HOL.uminus", _) $ t) = dest_coeff (~sign) t
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -23,22 +23,22 @@
 
 (*Utilities*)
 
-fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_binum n;
+fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
 
 (*Decodes a unary or binary numeral to a NATURAL NUMBER*)
-fun dest_numeral (Const ("HOL.zero", _)) = 0
-  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
-  | dest_numeral (Const("Numeral.number_of", _) $ w) =
-      (IntInf.max (0, HOLogic.dest_binum w)
-       handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
+fun dest_number (Const ("HOL.zero", _)) = 0
+  | dest_number (Const ("Suc", _) $ t) = 1 + dest_number t
+  | dest_number (Const("Numeral.number_of", _) $ w) =
+      (IntInf.max (0, HOLogic.dest_numeral w)
+       handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_number:1", [w]))
+  | dest_number t = raise TERM("Nat_Numeral_Simprocs.dest_number:2", [t]);
 
 fun find_first_numeral past (t::terms) =
-        ((dest_numeral t, t, rev past @ terms)
+        ((dest_number t, t, rev past @ terms)
          handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
-val zero = mk_numeral 0;
+val zero = mk_number 0;
 val mk_plus = HOLogic.mk_binop "HOL.plus";
 
 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
@@ -72,7 +72,7 @@
 
 (*** CancelNumerals simprocs ***)
 
-val one = mk_numeral 1;
+val one = mk_number 1;
 val mk_times = HOLogic.mk_binop "HOL.times";
 
 fun mk_prod [] = one
@@ -88,7 +88,7 @@
       handle TERM _ => [t];
 
 (*DON'T do the obvious simplifications; that would create special cases*)
-fun mk_coeff (k,t) = mk_times (mk_numeral k, t);
+fun mk_coeff (k,t) = mk_times (mk_number k, t);
 
 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
 fun dest_coeff t =
@@ -130,7 +130,7 @@
   in
      if relaxed orelse exists prod_has_numeral ts then 
        if k=0 then ts
-       else mk_numeral (IntInf.fromInt k) :: ts
+       else mk_number (IntInf.fromInt k) :: ts
      else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
   end;
 
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Integ/reflected_cooper.ML
--- a/src/HOL/Integ/reflected_cooper.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -20,7 +20,7 @@
       | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
       | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
       | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
+      | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
       | _ => error "i_of_term: unknown term";
 	
 
@@ -75,7 +75,7 @@
 
 fun term_of_i vs t =
     case t of 
-	Cst i => CooperDec.mk_numeral i
+	Cst i => CooperDec.mk_number i
       | Var n => valOf (myassoc2 vs n)
       | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
       | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Wed Dec 13 15:45:31 2006 +0100
@@ -140,10 +140,7 @@
 types_code
   nat ("int")
 attach (term_of) {*
-fun term_of_nat 0 = Const ("HOL.zero", HOLogic.natT)
-  | term_of_nat 1 = Const ("HOL.one", HOLogic.natT)
-  | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
-      HOLogic.mk_binum (IntInf.fromInt i);
+val term_of_nat = HOLogic.mk_number HOLogic.natT o InfInf.fromInt;
 *}
 attach (test) {*
 fun gen_nat i = random_range 0 i;
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Real/ferrante_rackoff_proof.ML
--- a/src/HOL/Real/ferrante_rackoff_proof.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -289,15 +289,8 @@
     (* Normalization of arithmetical expressions *)
 val rzero = Const("HOL.zero",rT);
 val rone = Const("HOL.one",rT);
-fun mk_real i = 
-    case i of 
-        0 => rzero
-      | 1 => rone
-      | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i); 
-
-fun dest_real (Const("HOL.zero",_)) = 0
-  | dest_real (Const("HOL.one",_)) = 1
-  | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
+fun mk_real i = HOLogic.mk_number rT i;
+val dest_real = snd o HOLogic.dest_number;
 
         (* Normal form for terms is: 
          (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Real/float.ML
--- a/src/HOL/Real/float.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Real/float.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -13,35 +13,35 @@
     type floatrep = IntInf.int * IntInf.int
     val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
     val approx_decstr_by_bin : int -> string -> floatrep * floatrep
-end 
+end
 =
 struct
 
 exception Destruct_floatstr of string;
 
-fun destruct_floatstr isDigit isExp number = 
+fun destruct_floatstr isDigit isExp number =
     let
 	val numlist = filter (not o Char.isSpace) (String.explode number)
-	
+
 	fun countsigns ((#"+")::cs) = countsigns cs
-	  | countsigns ((#"-")::cs) = 
-	    let	
-		val (positive, rest) = countsigns cs 
+	  | countsigns ((#"-")::cs) =
+	    let
+		val (positive, rest) = countsigns cs
 	    in
 		(not positive, rest)
 	    end
 	  | countsigns cs = (true, cs)
 
 	fun readdigits [] = ([], [])
-	  | readdigits (q as c::cs) = 
-	    if (isDigit c) then 
+	  | readdigits (q as c::cs) =
+	    if (isDigit c) then
 		let
 		    val (digits, rest) = readdigits cs
 		in
 		    (c::digits, rest)
 		end
 	    else
-		([], q)		
+		([], q)
 
 	fun readfromexp_helper cs =
 	    let
@@ -51,27 +51,27 @@
 		case rest' of
 		    [] => (positive, digits)
 		  | _ => raise (Destruct_floatstr number)
-	    end	    
+	    end
 
 	fun readfromexp [] = (true, [])
-	  | readfromexp (c::cs) = 
+	  | readfromexp (c::cs) =
 	    if isExp c then
 		readfromexp_helper cs
-	    else 
-		raise (Destruct_floatstr number)		
+	    else
+		raise (Destruct_floatstr number)
 
 	fun readfromdot [] = ([], readfromexp [])
-	  | readfromdot ((#".")::cs) = 
-	    let		
+	  | readfromdot ((#".")::cs) =
+	    let
 		val (digits, rest) = readdigits cs
 		val exp = readfromexp rest
 	    in
 		(digits, exp)
-	    end		
+	    end
 	  | readfromdot cs = readfromdot ((#".")::cs)
-			    
-	val (positive, numlist) = countsigns numlist				 
-	val (digits1, numlist) = readdigits numlist				 
+
+	val (positive, numlist) = countsigns numlist
+	val (digits1, numlist) = readdigits numlist
  	val (digits2, exp) = readfromdot numlist
     in
 	(positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
@@ -82,10 +82,10 @@
 exception Floating_point of string;
 
 val ln2_10 = (Math.ln 10.0)/(Math.ln 2.0)
-	
+
 fun intmul a b = IntInf.* (a,b)
-fun intsub a b = IntInf.- (a,b)	
-fun intadd a b = IntInf.+ (a,b) 		 
+fun intsub a b = IntInf.- (a,b)
+fun intadd a b = IntInf.+ (a,b) 
 fun intpow a b = IntInf.pow (a, IntInf.toInt b);
 fun intle a b = IntInf.<= (a, b);
 fun intless a b = IntInf.< (a, b);
@@ -96,33 +96,33 @@
 val ten = IntInf.fromInt 10;
 val five = IntInf.fromInt 5;
 
-fun find_most_significant q r = 
-    let 
-	fun int2real i = 
-	    case Real.fromString (IntInf.toString i) of 
-		SOME r => r 
-	      | NONE => raise (Floating_point "int2real")	
-	fun subtract (q, r) (q', r') = 
+fun find_most_significant q r =
+    let
+	fun int2real i =
+	    case Real.fromString (IntInf.toString i) of
+		SOME r => r
+	      | NONE => raise (Floating_point "int2real")
+	fun subtract (q, r) (q', r') =
 	    if intle r r' then
 		(intsub q (intmul q' (intpow ten (intsub r' r))), r)
 	    else
 		(intsub (intmul q (intpow ten (intsub r r'))) q', r')
 	fun bin2dec d =
-	    if intle zero d then 
+	    if intle zero d then
 		(intpow two d, zero)
 	    else
-		(intpow five (intneg d), d)				
-		
-	val L = IntInf.fromInt (Real.floor (int2real (IntInf.fromInt (IntInf.log2 q)) + (int2real r) * ln2_10))	
+		(intpow five (intneg d), d)
+
+	val L = IntInf.fromInt (Real.floor (int2real (IntInf.fromInt (IntInf.log2 q)) + (int2real r) * ln2_10))
 	val L1 = intadd L one
 
-	val (q1, r1) = subtract (q, r) (bin2dec L1) 		
+	val (q1, r1) = subtract (q, r) (bin2dec L1) 
     in
-	if intle zero q1 then 
+	if intle zero q1 then
 	    let
 		val (q2, r2) = subtract (q, r) (bin2dec (intadd L1 one))
 	    in
-		if intle zero q2 then 
+		if intle zero q2 then
 		    raise (Floating_point "find_most_significant")
 		else
 		    (L1, (q1, r1))
@@ -135,76 +135,76 @@
 		    (L, (q0, r0))
 		else
 		    raise (Floating_point "find_most_significant")
-	    end		    
+	    end
     end
 
 fun approx_dec_by_bin n (q,r) =
-    let	
+    let
 	fun addseq acc d' [] = acc
 	  | addseq acc d' (d::ds) = addseq (intadd acc (intpow two (intsub d d'))) d' ds
 
 	fun seq2bin [] = (zero, zero)
 	  | seq2bin (d::ds) = (intadd (addseq zero d ds) one, d)
 
-	fun approx d_seq d0 precision (q,r) = 
-	    if q = zero then 
+	fun approx d_seq d0 precision (q,r) =
+	    if q = zero then
 		let val x = seq2bin d_seq in
 		    (x, x)
 		end
-	    else    
-		let 
+	    else
+		let
 		    val (d, (q', r')) = find_most_significant q r
-		in	
-		    if intless precision (intsub d0 d) then 
-			let 
+		in
+		    if intless precision (intsub d0 d) then
+			let
 			    val d' = intsub d0 precision
 			    val x1 = seq2bin (d_seq)
-			    val x2 = (intadd (intmul (fst x1) (intpow two (intsub (snd x1) d'))) one,  d') (* = seq2bin (d'::d_seq) *) 
+			    val x2 = (intadd (intmul (fst x1) (intpow two (intsub (snd x1) d'))) one,  d') (* = seq2bin (d'::d_seq) *)
 			in
 			    (x1, x2)
 			end
 		    else
-			approx (d::d_seq) d0 precision (q', r') 						    		
-		end		
-	
+			approx (d::d_seq) d0 precision (q', r') 						    
+		end
+
 	fun approx_start precision (q, r) =
-	    if q = zero then 
+	    if q = zero then
 		((zero, zero), (zero, zero))
 	    else
-		let 
+		let
 		    val (d, (q', r')) = find_most_significant q r
-		in	
-		    if intle precision zero then 
+		in
+		    if intle precision zero then
 			let
 			    val x1 = seq2bin [d]
 			in
-			    if q' = zero then 
+			    if q' = zero then
 				(x1, x1)
 			    else
 				(x1, seq2bin [intadd d one])
 			end
 		    else
 			approx [d] d precision (q', r')
-		end		
+		end
     in
-	if intle zero q then 
+	if intle zero q then
 	    approx_start n (q,r)
 	else
-	    let 
-		val ((a1,b1), (a2, b2)) = approx_start n (intneg q, r) 
+	    let
+		val ((a1,b1), (a2, b2)) = approx_start n (intneg q, r)
 	    in
 		((intneg a2, b2), (intneg a1, b1))
-	    end					
+	    end
     end
 
 fun approx_decstr_by_bin n decstr =
-    let 
-	fun str2int s = case IntInf.fromString s of SOME x => x | NONE => zero 
+    let
+	fun str2int s = case IntInf.fromString s of SOME x => x | NONE => zero
 	fun signint p x = if p then x else intneg x
 
 	val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
 	val s = IntInf.fromInt (size d2)
-		
+
 	val q = signint p (intadd (intmul (str2int d1) (intpow ten s)) (str2int d2))
 	val r = intsub (signint ep (str2int e)) s
     in
@@ -213,10 +213,10 @@
 
 end;
 
-structure FloatArith = 
+structure FloatArith =
 struct
 
-type float = IntInf.int * IntInf.int 
+type float = IntInf.int * IntInf.int
 
 val izero = IntInf.fromInt 0
 val ione = IntInf.fromInt 1
@@ -228,30 +228,30 @@
 
 val floatzero = (izero, izero)
 
-fun positive_part (a,b) = 
+fun positive_part (a,b) =
     (if IntInf.< (a,izero) then izero else a, b)
 
-fun negative_part (a,b) = 
+fun negative_part (a,b) =
     (if IntInf.< (a,izero) then a else izero, b)
 
-fun is_negative (a,b) = 
+fun is_negative (a,b) =
     if IntInf.< (a, izero) then true else false
 
-fun is_positive (a,b) = 
+fun is_positive (a,b) =
     if IntInf.< (izero, a) then true else false
 
-fun is_zero (a,b) = 
+fun is_zero (a,b) =
     if a = izero then true else false
 
 fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
 
-fun add (a1, b1) (a2, b2) = 
+fun add (a1, b1) (a2, b2) =
     if IntInf.< (b1, b2) then
 	(iadd a1 (imul a2 (ipow2 (isub b2 b1))), b1)
     else
 	(iadd (imul a1 (ipow2 (isub b1 b2))) a2, b2)
 
-fun sub (a1, b1) (a2, b2) = 
+fun sub (a1, b1) (a2, b2) =
     if IntInf.< (b1, b2) then
 	(isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
     else
@@ -285,7 +285,7 @@
     exception Dest_intinf;
     val dest_intinf : term -> IntInf.int
     val dest_nat : term -> IntInf.int
-    
+
     exception Dest_float;
     val dest_float : term -> float
 
@@ -297,7 +297,7 @@
     val float_pprt_const : term
     val float_nprt_const : term
     val float_abs_const : term
-    val float_mult_const : term 
+    val float_mult_const : term
     val float_le_const : term
 
     val nat_le_const : term
@@ -314,8 +314,8 @@
 
     val invoke_float_op : term -> thm
     val invoke_nat_op : term -> thm*)
-end 
-= 
+end
+=
 struct
 
 structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
@@ -337,64 +337,31 @@
 val nat_le_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
 val nat_less_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
 val nat_eq_const = Const ("op =", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
- 		  
+ 
 val zero = FloatArith.izero
 val minus_one = FloatArith.imone
 val two = FloatArith.itwo
-	  
+
 exception Dest_intinf;
 exception Dest_float;
 
-fun mk_intinf ty n =
-  let
-    fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
-    fun bin_of n = 
-      if n = zero then HOLogic.pls_const
-      else if n = minus_one then HOLogic.min_const
-      else let 
-        val (q,r) = IntInf.divMod (n, two)
-      in
-        HOLogic.bit_const $ bin_of q $ mk_bit r
-      end
-  in 
-    HOLogic.number_of_const ty $ (bin_of n)
-  end
+fun mk_intinf ty n = HOLogic.number_of_const ty $ HOLogic.mk_numeral n;
 
-fun dest_intinf n = 
-    let
-	fun dest_bit n = 
-	    case n of 
-		Const ("Numeral.bit.B0", _) => FloatArith.izero
-	      | Const ("Numeral.bit.B1", _) => FloatArith.ione
-	      | _ => raise Dest_intinf
-			 
-	fun int_of n = 
-	    case n of
-		Const ("Numeral.Pls", _) => FloatArith.izero
-	      | Const ("Numeral.Min", _) => FloatArith.imone
-	      | Const ("Numeral.Bit", _) $ q $ r => FloatArith.iadd (FloatArith.imul (int_of q) FloatArith.itwo) (dest_bit r)
-	      | _ => raise Dest_intinf
-    in
-	case n of 
-	    Const ("Numeral.number_of", _) $ n' => int_of n'
-	  | Const ("Numeral0", _) => FloatArith.izero
-	  | Const ("Numeral1", _) => FloatArith.ione    
-	  | _ => raise Dest_intinf
-    end
+val dest_intinf = snd o HOLogic.dest_number
 
-fun mk_float (a,b) = 
+fun mk_float (a,b) =
     float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))
 
-fun dest_float f = 
-    case f of 
+fun dest_float f =
+    case f of
 	(Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) => (dest_intinf a, dest_intinf b)
       | Const ("Numeral.number_of",_) $ a => (dest_intinf f, 0)
       | Const ("Numeral0", _) => (FloatArith.izero, FloatArith.izero)
       | Const ("Numeral1", _) => (FloatArith.ione, FloatArith.izero)
       | _ => raise Dest_float
 
-fun dest_nat n = 
-    let 
+fun dest_nat n =
+    let
 	val v = dest_intinf n
     in
 	if IntInf.< (v, FloatArith.izero) then
@@ -403,7 +370,7 @@
 	    v
     end
 
-fun approx_float prec f value = 
+fun approx_float prec f value =
     let
 	val interval = ExactFloatingPoint.approx_decstr_by_bin prec value
 	val (flower, fupper) = f interval
@@ -415,26 +382,26 @@
 
 fun float_op_oracle (sg, exn as Float_op_oracle_data t) =
     Logic.mk_equals (t,
-		     case t of 
-			 f $ a $ b => 
-			 let 
-			     val a' = dest_float a 
+		     case t of
+			 f $ a $ b =>
+			 let
+			     val a' = dest_float a
 			     val b' = dest_float b
 			 in
 			     if f = float_add_const then
-				 mk_float (FloatArith.add a' b')	
+				 mk_float (FloatArith.add a' b')
 			     else if f = float_diff_const then
 				 mk_float (FloatArith.sub a' b')
 			     else if f = float_mult_const then
-				 mk_float (FloatArith.mul a' b')		
+				 mk_float (FloatArith.mul a' b')
 			     else if f = float_le_const then
 				 (if FloatArith.is_less b' a' then
 				     HOLogic.false_const
 				 else
 				     HOLogic.true_const)
-			     else raise exn	    		    	       
+			     else raise exn	    		    
 			 end
-		       | f $ a => 
+		       | f $ a =>
 			 let
 			     val a' = dest_float a
 			 in
@@ -454,7 +421,7 @@
 val th = ref ([]: theory list)
 val sg = ref ([]: Sign.sg list)
 
-fun invoke_float_op c = 
+fun invoke_float_op c =
     let
 	val th = (if length(!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
 	val sg = (if length(!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
@@ -466,10 +433,10 @@
 
 fun nat_op_oracle (sg, exn as Nat_op_oracle_data t) =
     Logic.mk_equals (t,
-		     case t of 
-			 f $ a $ b => 
-			 let 
-			     val a' = dest_nat a 
+		     case t of
+			 f $ a $ b =>
+			 let
+			     val a' = dest_nat a
 			     val b' = dest_nat b
 			 in
 			     if f = nat_le_const then
@@ -478,7 +445,7 @@
 				 else
 				     HOLogic.false_const)
 			     else if f = nat_eq_const then
-				 (if a' = b' then 
+				 (if a' = b' then
 				      HOLogic.true_const
 				  else
 				      HOLogic.false_const)
@@ -487,12 +454,13 @@
 				      HOLogic.true_const
 				  else
 				      HOLogic.false_const)
-			     else 
-				 raise exn	    	
+			     else
+				 raise exn
+
 			 end
 		       | _ => raise exn)
 
-fun invoke_nat_op c = 
+fun invoke_nat_op c =
     let
 	val th = (if length (!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
 	val sg = (if length (!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -11,8 +11,8 @@
 sig
   exception COOPER
   val is_arith_rel : term -> bool
-  val mk_numeral : IntInf.int -> term
-  val dest_numeral : term -> IntInf.int
+  val mk_number : IntInf.int -> term
+  val dest_number : term -> IntInf.int
   val is_numeral : term -> bool
   val zero : term
   val one : term
@@ -76,32 +76,32 @@
  
 (*Transform a natural number to a term*) 
  
-fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT)
-   |mk_numeral 1 = Const("HOL.one",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); 
+fun mk_number 0 = Const("HOL.zero",HOLogic.intT)
+   |mk_number 1 = Const("HOL.one",HOLogic.intT)
+   |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n); 
  
 (*Transform an Term to an natural number*)	  
 	  
-fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0
-   |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1
-   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
-       HOLogic.dest_binum n;
+fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0
+   |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1
+   |dest_number (Const ("Numeral.number_of",_) $ n) = 
+       HOLogic.dest_numeral n;
 (*Some terms often used for pattern matching*) 
  
-val zero = mk_numeral 0; 
-val one = mk_numeral 1; 
+val zero = mk_number 0; 
+val one = mk_number 1; 
  
 (*Tests if a Term is representing a number*) 
  
-fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_numeral t); 
+fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t); 
  
 (*maps a unary natural function on a term containing an natural number*) 
  
-fun numeral1 f n = mk_numeral (f(dest_numeral n)); 
+fun numeral1 f n = mk_number (f(dest_number n)); 
  
 (*maps a binary natural function on 2 term containing  natural numbers*) 
  
-fun numeral2 f m n = mk_numeral(f(dest_numeral m) (dest_numeral n)); 
+fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n)); 
  
 (* ------------------------------------------------------------------------- *) 
 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k          *) 
@@ -178,9 +178,9 @@
  Free(x,T)*) 
   
 fun lint vars tm = if is_numeral tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) 
+   (Free (x,T)) =>  (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero)) 
   |(Bound i) =>  (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) 
+  (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
   |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) 
   |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
   |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
@@ -188,8 +188,8 @@
         let val s' = lint vars s  
             val t' = lint vars t  
         in 
-        if is_numeral s' then (linear_cmul (dest_numeral s') t') 
-        else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
+        if is_numeral s' then (linear_cmul (dest_number s') t') 
+        else if is_numeral t' then (linear_cmul (dest_number t') s') 
  
          else raise COOPER
          end 
@@ -205,7 +205,7 @@
  
 fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
     if is_numeral c then   
-      let val c' = (mk_numeral(abs(dest_numeral c)))  
+      let val c' = (mk_number(abs(dest_number c)))  
       in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
@@ -214,11 +214,11 @@
   |linform vars  (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
   |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
   |linform vars  (Const("Orderings.less_eq",_)$ s $ t ) = 
-        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) 
+        (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
   |linform vars  (Const("op >=",_)$ s $ t ) = 
         (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> 
 	HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $s $(mk_numeral 1)) $ t)) 
+	HOLogic.intT) $s $(mk_number 1)) $ t)) 
  
    |linform vars  fm =  fm; 
  
@@ -228,7 +228,7 @@
  
 fun posineq fm = case fm of  
  (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
-   (HOLogic.mk_binrel "Orderings.less"  (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) ))) 
+   (HOLogic.mk_binrel "Orderings.less"  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
   | ( Const ("op &",_) $ p $ q)  => HOLogic.mk_conj (posineq p,posineq q)
   | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
   | _ => fm; 
@@ -245,7 +245,7 @@
  
 fun formlcm x fm = case fm of 
     (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) =>  if 
-    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
+    (is_arith_rel fm) andalso (x = y) then  (abs(dest_number c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
   | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
@@ -259,9 +259,9 @@
      case fm of  
       (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_numeral c) 
+        let val m = l div (dest_number c) 
             val n = (if p = "Orderings.less" then abs(m) else m) 
-            val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) 
+            val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x) 
 	in
         (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	end 
@@ -281,9 +281,9 @@
       if l = 1 then fm' 
 	 else 
      let val xp = (HOLogic.mk_binop "HOL.plus"  
-     		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
+     		((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero))
 	in 
-      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
+      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) 
       end 
   end; 
  
@@ -294,9 +294,9 @@
     case fm of  
       (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ 
       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_numeral c) 
+        let val m = l div (dest_number c) 
             val n = (if p = "Orderings.less" then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
+            val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x))
             in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
 	    end 
 	else fm 
@@ -320,7 +320,7 @@
   |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z 
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
-	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
+	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
 	          else error "minusinf : term not in normal form!!!"
 	else fm
 	 
@@ -341,7 +341,7 @@
   |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
   )) => if (x = y) 
 	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
-	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
 	     else error "plusinf : term not in normal form!!!"
 	else fm 
 
@@ -355,7 +355,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
-        if x = y then abs(dest_numeral d) else 1 
+        if x = y then abs(dest_number d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
   |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) 
@@ -375,7 +375,7 @@
    	  |_ =>[]) 
 			 
 			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))]  else [] 
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
   |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
   |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
   |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
@@ -395,8 +395,8 @@
    	  |_ =>[])
 
 			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a]  else []
-  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
+  |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
   |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
   |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
   |_ => [];
@@ -410,7 +410,7 @@
    ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => 
       if (x = y) andalso (is_arith_rel fm)  
       then  
-        let val ct = linear_cmul (dest_numeral c) t  
+        let val ct = linear_cmul (dest_number c) t  
 	in (HOLogic.mk_binrel p (d, linear_add vars ct z)) 
 	end 
 	else fm 
@@ -430,16 +430,16 @@
 fun dvd_op (d, t) = 
  if not(is_numeral d) then raise DVD_UNKNOWN
  else let 
-   val dn = dest_numeral d
+   val dn = dest_number d
    fun coeffs_of x = case x of 
      Const(p,_) $ tl $ tr => 
        if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr)
           else if p = "HOL.times" 
 	        then if (is_numeral tr) 
-		 then [(dest_numeral tr) * (dest_numeral tl)] 
-		 else [dest_numeral tl]
+		 then [(dest_number tr) * (dest_number tl)] 
+		 else [dest_number tl]
 	        else []
-    |_ => if (is_numeral t) then [dest_numeral t]  else []
+    |_ => if (is_numeral t) then [dest_number t]  else []
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
@@ -466,12 +466,12 @@
       handle _ => at)
     else
   case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
+    SOME f => ((if (f ((dest_number s),(dest_number t))) then 
     HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
       | _ =>  at) 
@@ -482,13 +482,13 @@
 fun evalc_atom at = case at of  
   (Const (p,_) $ s $ t) =>
    ( case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
+    SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const 
                 else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
+    SOME f => ((if (f ((dest_number s),(dest_number t))) 
                then HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
       | _ =>  at) 
@@ -659,8 +659,8 @@
     |mk_uni_vars T (Free (v,_)) = Free (v,T) 
     |mk_uni_vars T tm = tm; 
  
-fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2)) 
-    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2)) 
+fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2)) 
+    |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2)) 
     |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
     |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
     |mk_uni_int T tm = tm; 
@@ -680,8 +680,8 @@
     val p_inf = simpl (minusinf x p) 
     val bset = bset x p 
     val js = myupto 1 (divlcm x p)
-    fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p  
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)  
+    fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p  
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset)  
    in (list_disj (map stage js))
     end 
   | _ => error "cooper: not an existential formula"; 
@@ -699,8 +699,8 @@
     val p_inf = simpl (plusinf x p)
     val aset = aset x p
     val js = myupto 1 (divlcm x p)
-    fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
+    fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset)
    in (list_disj (map stage js))
    end
   | _ => error "cooper: not an existential formula";
@@ -711,13 +711,13 @@
 fun inf_w mi d vars x p = 
   let val f = if mi then minusinf else plusinf in
    case (simpl (minusinf x p)) of
-   Const("True",_)  => (SOME (mk_numeral 1), HOLogic.true_const)
+   Const("True",_)  => (SOME (mk_number 1), HOLogic.true_const)
   |Const("False",_) => (NONE,HOLogic.false_const)
   |F => 
       let 
       fun h n =
-       case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of 
-	Const("True",_) => (SOME (mk_numeral n),HOLogic.true_const)
+       case ((simpl o evalc) (linrep vars x (mk_number n) F)) of 
+	Const("True",_) => (SOME (mk_number n),HOLogic.true_const)
        |F' => if n=1 then (NONE,F')
 	     else let val (rw,rf) = h (n-1) in 
 	       (rw,HOLogic.mk_disj(F',rf))
@@ -736,7 +736,7 @@
              in (rw,HOLogic.mk_disj(F',rf)) 
 	     end)
     val f = if b then linear_add else linear_sub
-    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
+    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) []
     in h p_elements
     end;
 
@@ -769,8 +769,8 @@
     if (length bst) <= (length ast) 
      then (simpl (minusinf x p),linear_add,bst)
      else (simpl (plusinf x p), linear_sub,ast)
-    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+    fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
     fun stageh n = ((if n = 0 then []
 	else 
 	let 
@@ -805,8 +805,8 @@
      then (true,bst)
      else (false,ast)
     in withness d p_inf S vars x p 
-(*    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+(*    fun p_element j a = linrep vars x (f vars a (mk_number j)) p
+    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
    in (list_disj (map stage js))
 *)
    end
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -33,7 +33,7 @@
 val presburger_ss = simpset ()
   addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
 
-val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
+val cboolT = ctyp_of HOL.thy HOLogic.boolT;
 
 (*Theorems that will be used later for the proofgeneration*)
 
@@ -163,7 +163,7 @@
 fun norm_zero_one fm = case fm of
   (Const ("HOL.times",_) $ c $ t) => 
     if c = one then (norm_zero_one t)
-    else if (dest_numeral c = ~1) 
+    else if (dest_number c = ~1) 
          then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
          else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
@@ -253,18 +253,18 @@
 fun decomp_adjustcoeffeq sg x l fm = case fm of
     (Const("Not",_)$(Const("Orderings.less",_) $(Const("HOL.zero",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $    c $ y ) $z )))) => 
      let  
-        val m = l div (dest_numeral c) 
+        val m = l div (dest_number c) 
         val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) 
+        val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x)) 
         val rs = if (x = y) 
-                 then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
+                 then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) 
                  else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
-        val ck = cterm_of sg (mk_numeral n)
+        val ck = cterm_of sg (mk_number n)
         val cc = cterm_of sg c
         val ct = cterm_of sg z
         val cx = cterm_of sg y
         val pre = prove_elementar sg "lf" 
-            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral n)))
+            (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number n)))
         val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
         end
@@ -273,12 +273,12 @@
       c $ y ) $t )) => 
    if (is_arith_rel fm) andalso (x = y) 
    then  
-        let val m = l div (dest_numeral c) 
+        let val m = l div (dest_number c) 
            val k = (if p = "Orderings.less" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
+           val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div k)*l) ), x))
            val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) 
 
-           val ck = cterm_of sg (mk_numeral k)
+           val ck = cterm_of sg (mk_number k)
            val cc = cterm_of sg c
            val ct = cterm_of sg t
            val cx = cterm_of sg x
@@ -288,21 +288,21 @@
 	case p of
 	  "Orderings.less" => 
 	let val pre = prove_elementar sg "lf" 
-	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_numeral k)))
+	    (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),(mk_number k)))
             val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
 	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
          end
 
            |"op =" =>
 	     let val pre = prove_elementar sg "lf" 
-	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
 	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
              end
 
              |"Divides.dvd" =>
 	       let val pre = prove_elementar sg "lf" 
-	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
+	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_number k))))
                    val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
                in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
                         
@@ -574,7 +574,7 @@
 
    |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) =>
      if (is_arith_rel at) andalso (x=y)
-	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
+	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
 	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
 	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("HOL.one",HOLogic.intT))))
 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("HOL.zero",HOLogic.intT),dlcm))
@@ -675,7 +675,7 @@
 
    |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
         if (y=x) andalso (c1 =zero) then 
-        if pm1 = (mk_numeral ~1) then 
+        if pm1 = (mk_number ~1) then 
 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
               val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
 	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
@@ -734,7 +734,7 @@
     (Const (p,_) $ s $ t) =>(  
     case AList.lookup (op =) operations p of 
         SOME f => 
-           ((if (f ((dest_numeral s),(dest_numeral t))) 
+           ((if (f ((dest_number s),(dest_number t))) 
              then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
              else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
 		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
@@ -742,7 +742,7 @@
      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
        case AList.lookup (op =) operations p of 
          SOME f => 
-           ((if (f ((dest_numeral s),(dest_numeral t))) 
+           ((if (f ((dest_number s),(dest_number t))) 
              then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
              else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
 		      handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) 
@@ -842,14 +842,14 @@
    val ss = presburger_ss addsimps
      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
-   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
    (* e_ac_thm : Ex x. efm = EX x. fm*)
    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    (* A and B set of the formula*)
    val A = aset x cfm
    val B = bset x cfm
    (* the divlcm (delta) of the formula*)
-   val dlcm = mk_numeral (divlcm x cfm)
+   val dlcm = mk_number (divlcm x cfm)
    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    val cms = if ((length A) < (length B )) then "pi" else "mi"
 (*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
@@ -906,7 +906,7 @@
    val ss = presburger_ss addsimps
      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
-   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
    (* e_ac_thm : Ex x. efm = EX x. fm*)
    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
@@ -923,7 +923,7 @@
     val A = aset x cfm
     val B = bset x cfm
     (* the divlcm (delta) of the formula*)
-    val dlcm = mk_numeral (divlcm x cfm)
+    val dlcm = mk_number (divlcm x cfm)
     (* Which set is smaller to generate the (hoepfully) shorter proof*)
     val cms = if ((length A) < (length B )) then "pi" else "mi"
     (* synthesize the proof of cooper's theorem*)
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/Tools/Presburger/reflected_cooper.ML
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -20,7 +20,7 @@
       | Const ("HOL.plus",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
       | Const ("HOL.minus",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
       | Const ("HOL.times",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t')
+      | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_numeral t')
       | _ => error "i_of_term: unknown term";
 	
 
@@ -75,7 +75,7 @@
 
 fun term_of_i vs t =
     case t of 
-	Cst i => CooperDec.mk_numeral i
+	Cst i => CooperDec.mk_number i
       | Var n => valOf (myassoc2 vs n)
       | Neg t' => Const("HOL.uminus",iT --> iT)$(term_of_i vs t')
       | Add(t1,t2) => Const("HOL.plus",[iT,iT] ---> iT)$
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/arith_data.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -268,16 +268,16 @@
 
 exception Zero;
 
-fun rat_of_term (numt : term, dent : term) : Rat.rat =
-let
-  val num = HOLogic.dest_binum numt
-  val den = HOLogic.dest_binum dent
-in
-  if den = 0 then raise Zero else Rat.rat_of_quotient (num, den)
-end;
+fun rat_of_term (numt, dent) =
+  let
+    val num = HOLogic.dest_numeral numt
+    val den = HOLogic.dest_numeral dent
+  in
+    if den = 0 then raise Zero else Rat.rat_of_quotient (num, den)
+  end;
 
 (* Warning: in rare cases number_of encloses a non-numeral,
-   in which case dest_binum raises TERM; hence all the handles below.
+   in which case dest_numeral raises TERM; hence all the handles below.
    Same for Suc-terms that turn out not to be numerals -
    although the simplifier should eliminate those anyway ...
 *)
@@ -294,16 +294,16 @@
   fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
     (case s of
       Const ("Numeral.number_of", _) $ n =>
-        demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+        demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_numeral n)))
     | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
-        demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n))))
+        demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_numeral n))))
     | Const("Suc", _) $ _ =>
         demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s)))
     | Const ("HOL.times", _) $ s1 $ s2 =>
         demult (mC $ s1 $ (mC $ s2 $ t), m)
     | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
         let
-          val den = HOLogic.dest_binum dent
+          val den = HOLogic.dest_numeral dent
         in
           if den = 0 then
             raise Zero
@@ -316,7 +316,7 @@
   )
     | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
       (let
-        val den = HOLogic.dest_binum dent
+        val den = HOLogic.dest_numeral dent
       in
         if den = 0 then
           raise Zero
@@ -327,7 +327,7 @@
     | demult (Const ("HOL.zero", _), m) = (NONE, Rat.rat_of_int 0)
     | demult (Const ("HOL.one", _), m) = (NONE, m)
     | demult (t as Const ("Numeral.number_of", _) $ n, m) =
-        ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+        ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_numeral n)))
           handle TERM _ => (SOME t,m))
     | demult (Const ("HOL.uminus", _) $ t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
     | demult (t as Const f $ x, m) =
@@ -365,7 +365,7 @@
            (NONE,   m') => (p, Rat.add (i, m'))
          | (SOME u, m') => add_atom u m' pi)
     | poly (all as Const ("Numeral.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
-        (let val k = HOLogic.dest_binum t
+        (let val k = HOLogic.dest_numeral t
             val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
         in (p, Rat.add (i, Rat.mult (m, Rat.rat_of_intinf k2))) end
         handle TERM _ => add_atom all m pi)
@@ -427,8 +427,7 @@
   | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
   | domain_is_nat _                                                 = false;
 
-fun number_of (n : IntInf.int, T : typ) =
-  HOLogic.number_of_const T $ (HOLogic.mk_binum n);
+fun number_of (n, T) = HOLogic.mk_number T n;
 
 (*---------------------------------------------------------------------------*)
 (* code that performs certain goal transformations for linear arithmetic     *)
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -149,10 +149,7 @@
                become part of the Var's name*)
       | var (t,_) = fail t;
     (*translation of a literal*)
-    fun lit (Const("Numeral.number_of", _) $ w) =
-          (HOLogic.dest_binum w handle TERM _ => raise Match)
-      | lit (Const("0", _)) = 0
-      | lit (Const("1", _)) = 1
+    val lit = snd o HOLogic.dest_number;
     (*translation of a literal expression [no variables]*)
     fun litExp (Const("HOL.plus", T) $ x $ y) =
           if is_numeric_op T then (litExp x) + (litExp y)
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/HOL/hologic.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -78,27 +78,28 @@
   val B1_const: term
   val mk_bit: int -> term
   val dest_bit: term -> int
-  val intT: typ
   val pls_const: term
   val min_const: term
   val bit_const: term
   val number_of_const: typ -> term
-  val mk_binum: IntInf.int -> term
-  val dest_binum: term -> IntInf.int
-  val mk_int: IntInf.int -> term
+  val mk_numeral: IntInf.int -> term
+  val dest_numeral: term -> IntInf.int
+  val mk_number: typ -> IntInf.int -> term
+  val dest_number: term -> typ * IntInf.int
+  val intT: typ
   val realT: typ
+  val listT: typ -> typ
+  val mk_list: typ -> term list -> term
+  val dest_list: term -> term list
   val nibbleT: typ
   val mk_nibble: int -> term
   val dest_nibble: term -> int
   val charT: typ
   val mk_char: int -> term
   val dest_char: term -> int
-  val listT : typ -> typ
-  val mk_list: typ -> term list -> term
-  val dest_list: term -> term list
   val stringT: typ
-  val mk_string : string -> term
-  val dest_string : term -> string
+  val mk_string: string -> term
+  val dest_string: term -> string
 end;
 
 structure HOLogic: HOLOGIC =
@@ -323,24 +324,34 @@
 and min_const = Const ("Numeral.Min", intT)
 and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
 
-fun mk_binum 0 = pls_const
-  | mk_binum ~1 = min_const
-  | mk_binum i =
-      let val (q, r) = IntInf.divMod (i, 2)
-      in bit_const $ mk_binum q $ mk_bit (IntInf.toInt r) end;
-
-fun dest_binum (Const ("Numeral.Pls", _)) = 0
-  | dest_binum (Const ("Numeral.Min", _)) = ~1
-  | dest_binum (Const ("Numeral.Bit", _) $ bs $ b) =
-      2 * dest_binum bs + IntInf.fromInt (dest_bit b)
-  | dest_binum t = raise TERM ("dest_binum", [t]);
-
 fun number_of_const T = Const ("Numeral.number_of", intT --> T);
 
-fun mk_int 0 = Const ("HOL.zero", intT)
-  | mk_int 1 = Const ("HOL.one", intT)
-  | mk_int i = number_of_const intT $ mk_binum i;
+val mk_numeral =
+  let
+    fun mk_bit n = if n = 0 then B0_const else B1_const;
+    fun bin_of n =
+      if n = 0 then pls_const
+      else if n = ~1 then min_const
+      else
+        let
+          val (q, r) = IntInf.divMod (n, 2);
+        in bit_const $ bin_of q $ mk_bit r end;
+  in bin_of end;
 
+fun dest_numeral (Const ("Numeral.Pls", _)) = IntInf.fromInt 0
+  | dest_numeral (Const ("Numeral.Min", _)) = IntInf.fromInt ~1
+  | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
+      IntInf.fromInt (dest_bit b) + (2 * dest_numeral bs)
+  | dest_numeral t = raise TERM ("dest_numeral", [t]);
+
+fun mk_number T 0 = Const ("HOL.zero", T)
+  | mk_number T 1 = Const ("HOL.one", T)
+  | mk_number T i = number_of_const T $ mk_numeral i;
+
+fun dest_number (Const ("HOL.zero", T)) = (T, 0)
+  | dest_number (Const ("HOL.one", T)) = (T, 1)
+  | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t)
+  | dest_number t = raise TERM ("dest_number", [t]);
 
 (* real *)
 
@@ -403,7 +414,7 @@
 
 (* string *)
 
-val stringT = listT charT;
+val stringT = Type ("List.string", []);
 
 val mk_string = mk_list charT o map (mk_char o ord) o explode;
 val dest_string = implode o map (chr o dest_char) o dest_list;
diff -r 8eb82ffcdd15 -r 2f2b6a965ccc src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Dec 13 15:45:30 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Wed Dec 13 15:45:31 2006 +0100
@@ -15,7 +15,7 @@
 
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
-  val appgen_numeral: (theory -> term -> IntInf.int) -> appgen;
+  val appgen_numeral: (term -> IntInf.int option) -> appgen;
   val appgen_char: (term -> int option) -> appgen;
   val appgen_case: (theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
@@ -397,7 +397,7 @@
 (* (axiomatic extensions of extraction kernel *)
 
 fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
-  case try (int_of_numeral thy) (list_comb (Const c, ts))
+  case int_of_numeral (list_comb (Const c, ts))
    of SOME i =>
         trns
         |> pair (CodegenThingol.INum i)