simplified type int (eliminated IntInf.int, integer);
authorwenzelm
Tue Sep 18 16:08:00 2007 +0200 (2007-09-18)
changeset 24630351a308ab58d
parent 24629 65947eb930fa
child 24631 c7da302a0346
simplified type int (eliminated IntInf.int, integer);
src/HOL/Complex/ex/linreif.ML
src/HOL/Import/proof_kernel.ML
src/HOL/IntDiv.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Pretty_Char_chr.thy
src/HOL/Library/Pretty_Int.thy
src/HOL/Library/comm_ring.ML
src/HOL/Library/sct.ML
src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
src/HOL/Matrix/cplex/fspmlp.ML
src/HOL/Numeral.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/float_arith.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/ex/Binary.thy
src/HOL/ex/Random.thy
src/HOL/ex/coopereif.ML
src/HOL/ex/reflection.ML
src/HOL/ex/svc_funcs.ML
src/HOL/hologic.ML
src/HOL/int_arith1.ML
src/HOL/nat_simprocs.ML
src/Provers/Arith/cancel_factor.ML
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Syntax/lexicon.ML
src/Pure/library.ML
src/Tools/code/code_target.ML
src/Tools/float.ML
src/Tools/integer.ML
src/Tools/rat.ML
src/ZF/Tools/numeral_syntax.ML
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/src/HOL/Complex/ex/linreif.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/linreif.ML	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  open Ferrack;
     1.6  
     1.7 -val nat = Ferrack.nat o Integer.int;
     1.8 -
     1.9  exception LINR;
    1.10  
    1.11  (* pseudo reification : term -> intterm *)
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 18 11:06:22 2007 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 18 16:08:00 2007 +0200
     2.3 @@ -466,7 +466,7 @@
     2.4      end
     2.5  
     2.6  val protected_varnames = ref (Symtab.empty:string Symtab.table)
     2.7 -val invented_isavar = ref (IntInf.fromInt 0)
     2.8 +val invented_isavar = ref 0
     2.9  
    2.10  fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
    2.11  
    2.12 @@ -484,8 +484,8 @@
    2.13        SOME t => t
    2.14      | NONE => 
    2.15        let
    2.16 -	  val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
    2.17 -	  val t = "u_"^(IntInf.toString (!invented_isavar))
    2.18 +	  val _ = inc invented_isavar
    2.19 +	  val t = "u_" ^ string_of_int (!invented_isavar)
    2.20  	  val _ = ImportRecorder.protect_varname s t
    2.21            val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
    2.22        in
    2.23 @@ -499,8 +499,8 @@
    2.24  	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
    2.25  	| NONE => 	
    2.26            let
    2.27 -	      val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
    2.28 -	      val t = "u_"^(IntInf.toString (!invented_isavar))
    2.29 +	      val _ = inc invented_isavar
    2.30 +	      val t = "u_" ^ string_of_int (!invented_isavar)
    2.31                val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
    2.32            in
    2.33  	      ()
     3.1 --- a/src/HOL/IntDiv.thy	Tue Sep 18 11:06:22 2007 +0200
     3.2 +++ b/src/HOL/IntDiv.thy	Tue Sep 18 16:08:00 2007 +0200
     3.3 @@ -530,7 +530,7 @@
     3.4  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
     3.5    if n = 0 then NONE
     3.6    else
     3.7 -    let val (k, l) = IntInf.divMod (m, n);
     3.8 +    let val (k, l) = Integer.div_mod m n;
     3.9          fun mk_num x = HOLogic.mk_number HOLogic.intT x;
    3.10      in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
    3.11      end);
     4.1 --- a/src/HOL/Lambda/WeakNorm.thy	Tue Sep 18 11:06:22 2007 +0200
     4.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue Sep 18 16:08:00 2007 +0200
     4.3 @@ -425,8 +425,8 @@
     4.4  export_code type_NF nat int in SML module_name Norm
     4.5  
     4.6  ML {*
     4.7 -val nat_of_int = Norm.nat o IntInf.fromInt;
     4.8 -val int_of_nat = IntInf.toInt o Norm.int;
     4.9 +val nat_of_int = Norm.nat;
    4.10 +val int_of_nat = Norm.int;
    4.11  
    4.12  fun dBtype_of_typ (Type ("fun", [T, U])) =
    4.13        Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
     5.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Sep 18 11:06:22 2007 +0200
     5.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Sep 18 16:08:00 2007 +0200
     5.3 @@ -164,14 +164,14 @@
     5.4  *}
     5.5  
     5.6  code_type nat
     5.7 -  (SML "IntInf.int")
     5.8 +  (SML "int")
     5.9    (OCaml "Big'_int.big'_int")
    5.10    (Haskell "Integer")
    5.11  
    5.12  types_code
    5.13    nat ("int")
    5.14  attach (term_of) {*
    5.15 -val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
    5.16 +val term_of_nat = HOLogic.mk_number HOLogic.natT;
    5.17  *}
    5.18  attach (test) {*
    5.19  fun gen_nat i = random_range 0 i;
    5.20 @@ -224,7 +224,7 @@
    5.21      val simplify_less = Simplifier.rewrite 
    5.22        (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
    5.23      fun mk_rew (t, ty) =
    5.24 -      if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
    5.25 +      if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then
    5.26          Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
    5.27          |> simplify_less
    5.28          |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
     6.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Sep 18 11:06:22 2007 +0200
     6.2 +++ b/src/HOL/Library/Numeral_Type.thy	Tue Sep 18 16:08:00 2007 +0200
     6.3 @@ -168,12 +168,12 @@
     6.4        else if n = 0 then num0_const
     6.5        else if n = ~1 then raise TERM ("negative type numeral", [])
     6.6        else
     6.7 -        let val (q, r) = IntInf.divMod (n, 2);
     6.8 +        let val (q, r) = Integer.div_mod n 2;
     6.9          in mk_bit r $ bin_of q end;
    6.10    in bin_of n end;
    6.11  
    6.12  fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
    6.13 -      mk_bintype (valOf (IntInf.fromString str))
    6.14 +      mk_bintype (valOf (Int.fromString str))
    6.15    | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    6.16  
    6.17  in [("_NumeralType", numeral_tr)] end;
    6.18 @@ -182,7 +182,7 @@
    6.19  print_translation {*
    6.20  let
    6.21  fun int_of [] = 0
    6.22 -  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
    6.23 +  | int_of (b :: bs) = b + 2 * int_of bs;
    6.24  
    6.25  fun bin_of (Const ("num0", _)) = []
    6.26    | bin_of (Const ("num1", _)) = [1]
    6.27 @@ -194,7 +194,7 @@
    6.28    let
    6.29      val rev_digs = b :: bin_of t handle TERM _ => raise Match
    6.30      val i = int_of rev_digs;
    6.31 -    val num = IntInf.toString (IntInf.abs i);
    6.32 +    val num = string_of_int (abs i);
    6.33    in
    6.34      Syntax.const "_NumeralType" $ Syntax.free num
    6.35    end
     7.1 --- a/src/HOL/Library/Pretty_Char_chr.thy	Tue Sep 18 11:06:22 2007 +0200
     7.2 +++ b/src/HOL/Library/Pretty_Char_chr.thy	Tue Sep 18 16:08:00 2007 +0200
     7.3 @@ -38,7 +38,7 @@
     7.4    by (cases c) auto
     7.5  
     7.6  code_const int_of_char and char_of_int
     7.7 -  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
     7.8 +  (SML "!Char.ord" and "!Char.chr")
     7.9    (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    7.10    (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
    7.11  
     8.1 --- a/src/HOL/Library/Pretty_Int.thy	Tue Sep 18 11:06:22 2007 +0200
     8.2 +++ b/src/HOL/Library/Pretty_Int.thy	Tue Sep 18 16:08:00 2007 +0200
     8.3 @@ -16,7 +16,7 @@
     8.4  *}
     8.5  
     8.6  code_type int
     8.7 -  (SML "IntInf.int")
     8.8 +  (SML "int")
     8.9    (OCaml "Big'_int.big'_int")
    8.10    (Haskell "Integer")
    8.11  
    8.12 @@ -44,51 +44,51 @@
    8.13       and "error/ \"Bit\"")
    8.14  
    8.15  code_const Numeral.pred
    8.16 -  (SML "IntInf.- ((_), 1)")
    8.17 +  (SML "Int.- ((_), 1)")
    8.18    (OCaml "Big'_int.pred'_big'_int")
    8.19    (Haskell "!(_/ -/ 1)")
    8.20  
    8.21  code_const Numeral.succ
    8.22 -  (SML "IntInf.+ ((_), 1)")
    8.23 +  (SML "Int.+ ((_), 1)")
    8.24    (OCaml "Big'_int.succ'_big'_int")
    8.25    (Haskell "!(_/ +/ 1)")
    8.26  
    8.27  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    8.28 -  (SML "IntInf.+ ((_), (_))")
    8.29 +  (SML "Int.+ ((_), (_))")
    8.30    (OCaml "Big'_int.add'_big'_int")
    8.31    (Haskell infixl 6 "+")
    8.32  
    8.33  code_const "uminus \<Colon> int \<Rightarrow> int"
    8.34 -  (SML "IntInf.~")
    8.35 +  (SML "Int.~")
    8.36    (OCaml "Big'_int.minus'_big'_int")
    8.37    (Haskell "negate")
    8.38  
    8.39  code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    8.40 -  (SML "IntInf.- ((_), (_))")
    8.41 +  (SML "Int.- ((_), (_))")
    8.42    (OCaml "Big'_int.sub'_big'_int")
    8.43    (Haskell infixl 6 "-")
    8.44  
    8.45  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    8.46 -  (SML "IntInf.* ((_), (_))")
    8.47 +  (SML "Int.* ((_), (_))")
    8.48    (OCaml "Big'_int.mult'_big'_int")
    8.49    (Haskell infixl 7 "*")
    8.50  
    8.51  code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    8.52 -  (SML "!((_ : IntInf.int) = _)")
    8.53 +  (SML "!((_ : Int.int) = _)")
    8.54    (OCaml "Big'_int.eq'_big'_int")
    8.55    (Haskell infixl 4 "==")
    8.56  
    8.57  code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    8.58 -  (SML "IntInf.<= ((_), (_))")
    8.59 +  (SML "Int.<= ((_), (_))")
    8.60    (OCaml "Big'_int.le'_big'_int")
    8.61    (Haskell infix 4 "<=")
    8.62  
    8.63  code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    8.64 -  (SML "IntInf.< ((_), (_))")
    8.65 +  (SML "Int.< ((_), (_))")
    8.66    (OCaml "Big'_int.lt'_big'_int")
    8.67    (Haskell infix 4 "<")
    8.68  
    8.69 -code_reserved SML IntInf
    8.70 +code_reserved SML Int
    8.71  code_reserved OCaml Big_int
    8.72  
    8.73  end
    8.74 \ No newline at end of file
     9.1 --- a/src/HOL/Library/comm_ring.ML	Tue Sep 18 11:06:22 2007 +0200
     9.2 +++ b/src/HOL/Library/comm_ring.ML	Tue Sep 18 16:08:00 2007 +0200
     9.3 @@ -46,7 +46,7 @@
     9.4        in if i = 0
     9.5          then pol_PX T $ (pol_Pc T $ cring_one T)
     9.6            $ one $ (pol_Pc T $ cring_zero T)
     9.7 -        else pol_Pinj T $ HOLogic.mk_nat (Integer.int i)
     9.8 +        else pol_Pinj T $ HOLogic.mk_nat i
     9.9            $ (pol_PX T $ (pol_Pc T $ cring_one T)
    9.10              $ one $ (pol_Pc T $ cring_zero T))
    9.11          end
    10.1 --- a/src/HOL/Library/sct.ML	Tue Sep 18 11:06:22 2007 +0200
    10.2 +++ b/src/HOL/Library/sct.ML	Tue Sep 18 16:08:00 2007 +0200
    10.3 @@ -157,8 +157,8 @@
    10.4        measures
    10.5      end
    10.6  
    10.7 -val mk_number = HOLogic.mk_nat o IntInf.fromInt
    10.8 -val dest_number = IntInf.toInt o HOLogic.dest_nat
    10.9 +val mk_number = HOLogic.mk_nat
   10.10 +val dest_number = HOLogic.dest_nat
   10.11  
   10.12  fun nums_to i = map mk_number (0 upto (i - 1))
   10.13  
    11.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Sep 18 11:06:22 2007 +0200
    11.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Sep 18 16:08:00 2007 +0200
    11.3 @@ -14,9 +14,9 @@
    11.4    val approx_vector : int -> (float -> float) -> vector -> term * term
    11.5    val approx_matrix : int -> (float -> float) -> matrix -> term * term
    11.6  
    11.7 -  val mk_spvec_entry : integer -> float -> term
    11.8 -  val mk_spvec_entry' : integer -> term -> term
    11.9 -  val mk_spmat_entry : integer -> term -> term
   11.10 +  val mk_spvec_entry : int -> float -> term
   11.11 +  val mk_spvec_entry' : int -> term -> term
   11.12 +  val mk_spmat_entry : int -> term -> term
   11.13    val spvecT: typ
   11.14    val spmatT: typ
   11.15    
   11.16 @@ -76,7 +76,7 @@
   11.17      fun app (index, s) (lower, upper) =
   11.18        let
   11.19          val (flower, fupper) = approx_value prec pprt s
   11.20 -        val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
   11.21 +        val index = HOLogic.mk_number HOLogic.natT index
   11.22          val elower = HOLogic.mk_prod (index, flower)
   11.23          val eupper = HOLogic.mk_prod (index, fupper)
   11.24        in (elower :: lower, eupper :: upper) end;
   11.25 @@ -89,7 +89,7 @@
   11.26      fun app (index, v) (lower, upper) =
   11.27        let
   11.28          val (flower, fupper) = approx_vector prec pprt v
   11.29 -        val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
   11.30 +        val index = HOLogic.mk_number HOLogic.natT index
   11.31          val elower = HOLogic.mk_prod (index, flower)
   11.32          val eupper = HOLogic.mk_prod (index, fupper)
   11.33        in (elower :: lower, eupper :: upper) end;
    12.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Tue Sep 18 11:06:22 2007 +0200
    12.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Tue Sep 18 16:08:00 2007 +0200
    12.3 @@ -284,11 +284,10 @@
    12.4                      val index = xlen-i
    12.5                      val (r12_1, r12_2) = abs_estimate (i-1) r1 r2
    12.6                      val b1 = Inttab.lookup r1 index
    12.7 -                    val b2 = Inttab.lookup r2 index 
    12.8 -                    val i' = Integer.int index
    12.9 +                    val b2 = Inttab.lookup r2 index
   12.10                  in
   12.11 -                    (add_row_entry r12_1 i' @{term "lbound :: real => real"} ((names index)^"l") b1, 
   12.12 -		     add_row_entry r12_2 i' @{term "ubound :: real => real"} ((names index)^"u") b2)
   12.13 +                    (add_row_entry r12_1 index @{term "lbound :: real => real"} ((names index)^"l") b1, 
   12.14 +		     add_row_entry r12_2 index @{term "ubound :: real => real"} ((names index)^"u") b2)
   12.15                  end
   12.16  
   12.17          val (r1, r2) = abs_estimate xlen r1 r2
    13.1 --- a/src/HOL/Numeral.thy	Tue Sep 18 11:06:22 2007 +0200
    13.2 +++ b/src/HOL/Numeral.thy	Tue Sep 18 16:08:00 2007 +0200
    13.3 @@ -635,12 +635,10 @@
    13.4  code_modulename Haskell
    13.5    Numeral Integer
    13.6  
    13.7 -(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
    13.8 -
    13.9  types_code
   13.10    "int" ("int")
   13.11  attach (term_of) {*
   13.12 -val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
   13.13 +val term_of_int = HOLogic.mk_number HOLogic.intT;
   13.14  *}
   13.15  attach (test) {*
   13.16  fun gen_int i = one_of [~1, 1] * random_range 0 i;
   13.17 @@ -656,7 +654,7 @@
   13.18    let val i = HOLogic.dest_numeral (strip_number_of t)
   13.19    in
   13.20      SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
   13.21 -      Pretty.str (IntInf.toString i))
   13.22 +      Pretty.str (string_of_int i))
   13.23    end handle TERM _ => NONE;
   13.24  
   13.25  in
    14.1 --- a/src/HOL/Real/Rational.thy	Tue Sep 18 11:06:22 2007 +0200
    14.2 +++ b/src/HOL/Real/Rational.thy	Tue Sep 18 16:08:00 2007 +0200
    14.3 @@ -697,8 +697,8 @@
    14.4      val p = random_range 0 i;
    14.5      val q = random_range 1 (i + 1);
    14.6      val g = Integer.gcd p q;
    14.7 -    val p' = Integer.div p g;
    14.8 -    val q' = Integer.div q g;
    14.9 +    val p' = p div g;
   14.10 +    val q' = q div g;
   14.11    in
   14.12      (if one_of [true, false] then p' else ~ p',
   14.13       if p' = 0 then 0 else q')
    15.1 --- a/src/HOL/Real/RealDef.thy	Tue Sep 18 11:06:22 2007 +0200
    15.2 +++ b/src/HOL/Real/RealDef.thy	Tue Sep 18 16:08:00 2007 +0200
    15.3 @@ -1011,8 +1011,8 @@
    15.4      val p = random_range 0 i;
    15.5      val q = random_range 1 (i + 1);
    15.6      val g = Integer.gcd p q;
    15.7 -    val p' = Integer.div p g;
    15.8 -    val q' = Integer.div q g;
    15.9 +    val p' = p div g;
   15.10 +    val q' = q div g;
   15.11    in
   15.12      (if one_of [true, false] then p' else ~ p',
   15.13       if p' = 0 then 0 else q')
    16.1 --- a/src/HOL/Real/float_arith.ML	Tue Sep 18 11:06:22 2007 +0200
    16.2 +++ b/src/HOL/Real/float_arith.ML	Tue Sep 18 16:08:00 2007 +0200
    16.3 @@ -9,7 +9,7 @@
    16.4    val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
    16.5  
    16.6    exception Floating_point of string
    16.7 -  val approx_dec_by_bin: integer -> Float.float -> Float.float * Float.float
    16.8 +  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
    16.9    val approx_decstr_by_bin: int -> string -> Float.float * Float.float
   16.10  
   16.11    val mk_float: Float.float -> term
   16.12 @@ -91,30 +91,30 @@
   16.13  fun find_most_significant q r =
   16.14    let
   16.15      fun int2real i =
   16.16 -      case (Real.fromString o Integer.string_of_int) i of
   16.17 +      case (Real.fromString o string_of_int) i of
   16.18          SOME r => r
   16.19          | NONE => raise (Floating_point "int2real")
   16.20      fun subtract (q, r) (q', r') =
   16.21 -      if r <=% r' then
   16.22 +      if r <= r' then
   16.23          (q - q' * exp10 (r' - r), r)
   16.24        else
   16.25          (q * exp10 (r - r') - q', r')
   16.26      fun bin2dec d =
   16.27 -      if 0 <=% d then
   16.28 -        (Integer.exp d, 0)
   16.29 +      if 0 <= d then
   16.30 +        (Integer.square d, 0)
   16.31        else
   16.32          (exp5 (~ d), d)
   16.33  
   16.34 -    val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10))
   16.35 +    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
   16.36      val L1 = L + 1
   16.37  
   16.38      val (q1, r1) = subtract (q, r) (bin2dec L1) 
   16.39    in
   16.40 -    if 0 <=% q1 then
   16.41 +    if 0 <= q1 then
   16.42        let
   16.43          val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
   16.44        in
   16.45 -        if 0 <=% q2 then
   16.46 +        if 0 <= q2 then
   16.47            raise (Floating_point "find_most_significant")
   16.48          else
   16.49            (L1, (q1, r1))
   16.50 @@ -123,7 +123,7 @@
   16.51        let
   16.52          val (q0, r0) = subtract (q, r) (bin2dec L)
   16.53        in
   16.54 -        if 0 <=% q0 then
   16.55 +        if 0 <= q0 then
   16.56            (L, (q0, r0))
   16.57          else
   16.58            raise (Floating_point "find_most_significant")
   16.59 @@ -133,10 +133,10 @@
   16.60  fun approx_dec_by_bin n (q,r) =
   16.61    let
   16.62      fun addseq acc d' [] = acc
   16.63 -      | addseq acc d' (d::ds) = addseq (acc +% Integer.exp (d - d')) d' ds
   16.64 +      | addseq acc d' (d::ds) = addseq (acc + Integer.square (d - d')) d' ds
   16.65  
   16.66      fun seq2bin [] = (0, 0)
   16.67 -      | seq2bin (d::ds) = (addseq 0 d ds +% 1, d)
   16.68 +      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
   16.69  
   16.70      fun approx d_seq d0 precision (q,r) =
   16.71        if q = 0 then
   16.72 @@ -147,11 +147,11 @@
   16.73          let
   16.74            val (d, (q', r')) = find_most_significant q r
   16.75          in
   16.76 -          if precision <% d0 - d then
   16.77 +          if precision < d0 - d then
   16.78              let
   16.79                val d' = d0 - precision
   16.80                val x1 = seq2bin (d_seq)
   16.81 -              val x2 = (fst x1 * Integer.exp (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
   16.82 +              val x2 = (fst x1 * Integer.square (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
   16.83              in
   16.84                (x1, x2)
   16.85              end
   16.86 @@ -160,26 +160,26 @@
   16.87          end
   16.88  
   16.89      fun approx_start precision (q, r) =
   16.90 -      if q =% 0 then
   16.91 +      if q = 0 then
   16.92          ((0, 0), (0, 0))
   16.93        else
   16.94          let
   16.95            val (d, (q', r')) = find_most_significant q r
   16.96          in
   16.97 -          if precision <=% 0 then
   16.98 +          if precision <= 0 then
   16.99              let
  16.100                val x1 = seq2bin [d]
  16.101              in
  16.102                if q' = 0 then
  16.103                  (x1, x1)
  16.104                else
  16.105 -                (x1, seq2bin [d +% 1])
  16.106 +                (x1, seq2bin [d + 1])
  16.107              end
  16.108            else
  16.109              approx [d] d precision (q', r')
  16.110          end
  16.111    in
  16.112 -    if 0 <=% q then
  16.113 +    if 0 <= q then
  16.114        approx_start n (q,r)
  16.115      else
  16.116        let
  16.117 @@ -191,16 +191,16 @@
  16.118  
  16.119  fun approx_decstr_by_bin n decstr =
  16.120    let
  16.121 -    fun str2int s = the_default 0 (Integer.int_of_string s);
  16.122 -    fun signint p x = if p then x else Integer.neg x
  16.123 +    fun str2int s = the_default 0 (Int.fromString s)
  16.124 +    fun signint p x = if p then x else ~ x
  16.125  
  16.126      val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
  16.127 -    val s = Integer.int (size d2)
  16.128 +    val s = size d2
  16.129  
  16.130      val q = signint p (str2int d1 * exp10 s + str2int d2)
  16.131      val r = signint ep (str2int e) - s
  16.132    in
  16.133 -    approx_dec_by_bin (Integer.int n) (q,r)
  16.134 +    approx_dec_by_bin n (q,r)
  16.135    end
  16.136  
  16.137  fun mk_float (a, b) = @{term "float"} $
    17.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Sep 18 11:06:22 2007 +0200
    17.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Sep 18 16:08:00 2007 +0200
    17.3 @@ -41,8 +41,8 @@
    17.4  (* ------------------------------------------------------------------------- *)
    17.5  
    17.6  datatype history =
    17.7 -   Start of integer
    17.8 - | Mmul of (Rat.rat * (integer list)) * history
    17.9 +   Start of int
   17.10 + | Mmul of (Rat.rat * int list) * history
   17.11   | Add of history * history;
   17.12  
   17.13  
   17.14 @@ -54,8 +54,8 @@
   17.15                  ([],[]) => false
   17.16                | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
   17.17                | _ => error "morder: inconsistent monomial lengths"
   17.18 -        val n1 = fold Integer.add m1 0
   17.19 -        val n2 = fold Integer.add m2 0 in
   17.20 +        val n1 = Integer.sum m1
   17.21 +        val n2 = Integer.sum m2 in
   17.22      n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
   17.23      end;
   17.24  
   17.25 @@ -80,7 +80,7 @@
   17.26  
   17.27  fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
   17.28  
   17.29 -fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 Integer.add m1 m2);
   17.30 +fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
   17.31  
   17.32  fun grob_cmul cm pol = map (grob_mmul cm) pol;
   17.33  
   17.34 @@ -108,29 +108,27 @@
   17.35  fun grob_pow vars l n =
   17.36    if n < 0 then error "grob_pow: negative power"
   17.37    else if n = 0 then [(rat_1,map (fn v => 0) vars)]
   17.38 -  else grob_mul l (grob_pow vars l (n -% 1));
   17.39 -
   17.40 -val max = fn (x: integer) => fn y => if x < y then y else x;
   17.41 +  else grob_mul l (grob_pow vars l (n - 1));
   17.42  
   17.43  fun degree vn p =
   17.44   case p of
   17.45    [] => error "Zero polynomial"
   17.46  | [(c,ns)] => nth ns vn
   17.47 -| (c,ns)::p' => max (nth ns vn) (degree vn p');
   17.48 +| (c,ns)::p' => Int.max (nth ns vn, degree vn p');
   17.49  
   17.50  fun head_deg vn p = let val d = degree vn p in
   17.51   (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end;
   17.52  
   17.53 -val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) (0: integer)) ns);
   17.54 +val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
   17.55  val grob_pdiv =
   17.56   let fun pdiv_aux vn (n,a) p k s =
   17.57    if is_zerop s then (k,s) else
   17.58    let val (m,b) = head_deg vn s
   17.59    in if m < n then (k,s) else
   17.60 -     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m -% n else 0)
   17.61 +     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
   17.62                                                  (snd (hd s)))]
   17.63       in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
   17.64 -        else pdiv_aux vn (n,a) p (k +% 1) (grob_sub (grob_mul a s) (grob_mul b p'))
   17.65 +        else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
   17.66       end
   17.67    end
   17.68   in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
   17.69 @@ -140,11 +138,11 @@
   17.70  
   17.71  fun mdiv (c1,m1) (c2,m2) =
   17.72    (c1//c2,
   17.73 -   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 -% n2) m1 m2);
   17.74 +   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
   17.75  
   17.76  (* Lowest common multiple of two monomials. *)
   17.77  
   17.78 -fun mlcm (c1,m1) (c2,m2) = (rat_1,map2 max m1 m2);
   17.79 +fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2));
   17.80  
   17.81  (* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
   17.82  
   17.83 @@ -221,7 +219,7 @@
   17.84    | _ => false;
   17.85  
   17.86  fun poly_eq p1 p2 =
   17.87 -  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: integer list) = m2) p1 p2;
   17.88 +  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
   17.89  
   17.90  fun memx ((p1,h1),(p2,h2)) ppairs =
   17.91    not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
   17.92 @@ -237,7 +235,7 @@
   17.93  (* Test for hitting constant polynomial.                                     *)
   17.94  
   17.95  fun constant_poly p =
   17.96 -  length p = 1 andalso forall (fn x => x = (0: integer)) (snd(hd p));
   17.97 +  length p = 1 andalso forall (fn x => x = 0) (snd(hd p));
   17.98  
   17.99  (* ------------------------------------------------------------------------- *)
  17.100  (* Grobner basis algorithm.                                                  *)
  17.101 @@ -299,8 +297,7 @@
  17.102  (* ------------------------------------------------------------------------- *)
  17.103  
  17.104  fun grobner pols =
  17.105 -    let val npols = map2 (fn p => fn n => (p,Start n)) pols
  17.106 -          (map Integer.int (0 upto (length pols - 1)))
  17.107 +    let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
  17.108          val phists = filter (fn (p,_) => not (null p)) npols
  17.109          val bas = grobner_interreduce [] (map monic phists)
  17.110          val prs0 = product bas bas
  17.111 @@ -376,7 +373,7 @@
  17.112          val pol' = augment pol
  17.113          val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
  17.114          val (l,cert) = grobner_weak vars' allpols
  17.115 -        val d = fold_rev (fold_rev (max o hd o snd) o snd) cert 0
  17.116 +        val d = fold_rev (fold_rev (curry Int.max o hd o snd) o snd) cert 0
  17.117          fun transform_monomial (c,m) =
  17.118              grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
  17.119          fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
  17.120 @@ -575,7 +572,7 @@
  17.121   let fun holify_varpow (v,n) =
  17.122    if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
  17.123   fun holify_monomial vars (c,m) =
  17.124 -  let val xps = map holify_varpow (filter (fn (_,n) => n <> (0: integer)) (vars ~~ m))
  17.125 +  let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
  17.126     in end_itlist ring_mk_mul (mk_const c :: xps)
  17.127    end
  17.128   fun holify_polynomial vars p =
  17.129 @@ -624,7 +621,7 @@
  17.130            grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
  17.131         val (deg,l,cert) = grobner_strong vars pols pol
  17.132         val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
  17.133 -       val th2 = funpow (Integer.machine_int deg) (idom_rule o HOLogic.conj_intr th1) neq_01
  17.134 +       val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01
  17.135        in (vars,l,cert,th2)
  17.136        end)
  17.137  (*    val _ = writeln ("Translating certificate to HOL inferences") *)
  17.138 @@ -637,7 +634,7 @@
  17.139          if null pols then reflexive(mk_const rat_0) else
  17.140          end_itlist mk_add
  17.141              (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p)
  17.142 -              (nth eths (Integer.machine_int i) |> mk_meta_eq)) pols)
  17.143 +              (nth eths i |> mk_meta_eq)) pols)
  17.144      val th1 = thm_fn herts_pos
  17.145      val th2 = thm_fn herts_neg
  17.146      val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
  17.147 @@ -681,7 +678,7 @@
  17.148    val pol = grobify_term vars tm
  17.149    val cert = grobner_ideal vars pols pol
  17.150   in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
  17.151 -        (map Integer.int (0 upto (length pols - 1)))
  17.152 +        (0 upto (length pols - 1))
  17.153   end
  17.154  in (ring,ideal)
  17.155  end;
    18.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Sep 18 11:06:22 2007 +0200
    18.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Sep 18 16:08:00 2007 +0200
    18.3 @@ -14,7 +14,6 @@
    18.4  
    18.5  open Conv;
    18.6  open Normalizer;
    18.7 -structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
    18.8  
    18.9  exception COOPER of string * exn;
   18.10  val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
   18.11 @@ -178,10 +177,10 @@
   18.12    | linear_cmul n tm = 
   18.13      case tm of  
   18.14        Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b)
   18.15 -    | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (Integer.mult n) c)$x
   18.16 +    | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (fn m => n * m) c)$x
   18.17      | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b)
   18.18      | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a)
   18.19 -    | _ =>  numeral1 (Integer.mult n) tm;
   18.20 +    | _ =>  numeral1 (fn m => n * m) tm;
   18.21  fun earlier [] x y = false 
   18.22  	| earlier (h::t) x y = 
   18.23      if h aconv y then false else if h aconv x then true else earlier t x y; 
   18.24 @@ -191,7 +190,7 @@
   18.25  	 (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1,
   18.26      Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => 
   18.27     if x1 = x2 then 
   18.28 -     let val c = numeral2 Integer.add c1 c2
   18.29 +     let val c = numeral2 (curry op +) c1 c2
   18.30  	   in if c = zero then linear_add vars r1  r2  
   18.31  	      else addC$(mulC$c$x1)$(linear_add vars  r1 r2)
   18.32       end 
   18.33 @@ -201,7 +200,7 @@
   18.34      	  addC$(mulC$c1$x1)$(linear_add vars r1 tm2)
   18.35   | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => 
   18.36        	  addC$(mulC$c2$x2)$(linear_add vars tm1 r2) 
   18.37 - | (_,_) => numeral2 Integer.add tm1 tm2;
   18.38 + | (_,_) => numeral2 (curry op +) tm1 tm2;
   18.39   
   18.40  fun linear_neg tm = linear_cmul ~1 tm; 
   18.41  fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
   18.42 @@ -294,7 +293,7 @@
   18.43   let
   18.44    val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
   18.45    val x = term_of cx 
   18.46 -  val ins = insert (op = : integer*integer -> bool)
   18.47 +  val ins = insert (op = : int * int -> bool)
   18.48    fun h (acc,dacc) t = 
   18.49     case (term_of t) of
   18.50      Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
   18.51 @@ -312,7 +311,7 @@
   18.52    | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)
   18.53    | _ => (acc, dacc)
   18.54    val (cs,ds) = h ([],[]) p
   18.55 -  val l = fold Integer.lcm (cs union ds) 1
   18.56 +  val l = Integer.lcms (cs union ds)
   18.57    fun cv k ct = 
   18.58      let val (tm as b$s$t) = term_of ct 
   18.59      in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
   18.60 @@ -325,10 +324,10 @@
   18.61             (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) 
   18.62             @{cterm "0::int"})))
   18.63     in equal_elim (Thm.symmetric th) TrueI end;
   18.64 -  val notz = let val tab = fold Integertab.update 
   18.65 -                               (ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty 
   18.66 +  val notz = let val tab = fold Inttab.update 
   18.67 +                               (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty 
   18.68              in 
   18.69 -             (fn ct => (valOf (Integertab.lookup tab (ct |> term_of |> dest_numeral)) 
   18.70 +             (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) 
   18.71                  handle Option => (writeln "noz: Theorems-Table contains no entry for"; 
   18.72                                      print_cterm ct ; raise Option)))
   18.73             end
   18.74 @@ -340,15 +339,15 @@
   18.75    | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
   18.76      if x=y andalso member (op =)
   18.77        ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   18.78 -    then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
   18.79 +    then cv (l div dest_numeral c) t else Thm.reflexive t
   18.80    | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
   18.81      if x=y andalso member (op =)
   18.82        [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
   18.83 -    then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
   18.84 +    then cv (l div dest_numeral c) t else Thm.reflexive t
   18.85    | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => 
   18.86      if x=y then 
   18.87        let 
   18.88 -       val k = Integer.div l (dest_numeral c)
   18.89 +       val k = l div dest_numeral c
   18.90         val kt = HOLogic.mk_number iT k
   18.91         val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] 
   18.92               ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
   18.93 @@ -384,7 +383,6 @@
   18.94  
   18.95  val D_tm = @{cpat "?D::int"};
   18.96  
   18.97 -val int_eq = (op =):integer*integer -> bool;
   18.98  fun cooperex_conv ctxt vs q = 
   18.99  let 
  18.100  
  18.101 @@ -403,11 +401,11 @@
  18.102    | Le t => (bacc, ins (plus1 t) aacc,dacc)
  18.103    | Gt t => (ins t bacc, aacc,dacc)
  18.104    | Ge t => (ins (minus1 t) bacc, aacc,dacc)
  18.105 -  | Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc)
  18.106 -  | NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc)
  18.107 +  | Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
  18.108 +  | NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
  18.109    | _ => (bacc, aacc, dacc)
  18.110   val (b0,a0,ds) = h p ([],[],[])
  18.111 - val d = fold Integer.lcm ds 1
  18.112 + val d = Integer.lcms ds
  18.113   val cd = Numeral.mk_cnumber @{ctyp "int"} d
  18.114   val dt = term_of cd
  18.115   fun divprop x = 
  18.116 @@ -417,9 +415,9 @@
  18.117        (Thm.capply @{cterm Trueprop} 
  18.118             (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
  18.119     in equal_elim (Thm.symmetric th) TrueI end;
  18.120 - val dvd = let val tab = fold Integertab.update
  18.121 -                               (ds ~~ (map divprop ds)) Integertab.empty in 
  18.122 -           (fn ct => (valOf (Integertab.lookup tab (term_of ct |> dest_numeral)) 
  18.123 + val dvd = let val tab = fold Inttab.update
  18.124 +                               (ds ~~ (map divprop ds)) Inttab.empty in 
  18.125 +           (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) 
  18.126                      handle Option => (writeln "dvd: Theorems-Table contains no entry for"; 
  18.127                                        print_cterm ct ; raise Option)))
  18.128             end
  18.129 @@ -545,7 +543,7 @@
  18.130        | SOME n => Bound n)
  18.131    | @{term "0::int"} => C 0
  18.132    | @{term "1::int"} => C 1
  18.133 -  | Term.Bound i => Bound (Integer.int i)
  18.134 +  | Term.Bound i => Bound i
  18.135    | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
  18.136    | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
  18.137    | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
  18.138 @@ -641,8 +639,7 @@
  18.139  
  18.140  fun cooper_oracle thy t = 
  18.141    let
  18.142 -    val (vs, ps) = pairself (map_index (swap o apfst Integer.int))
  18.143 -      (term_frees t, term_bools [] t);
  18.144 +    val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
  18.145    in
  18.146      equals propT $ HOLogic.mk_Trueprop t $
  18.147        HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
    19.1 --- a/src/HOL/Tools/numeral.ML	Tue Sep 18 11:06:22 2007 +0200
    19.2 +++ b/src/HOL/Tools/numeral.ML	Tue Sep 18 16:08:00 2007 +0200
    19.3 @@ -7,8 +7,8 @@
    19.4  
    19.5  signature NUMERAL =
    19.6  sig
    19.7 -  val mk_cnumeral: integer -> cterm
    19.8 -  val mk_cnumber: ctyp -> integer -> cterm
    19.9 +  val mk_cnumeral: int -> cterm
   19.10 +  val mk_cnumber: ctyp -> int -> cterm
   19.11  end;
   19.12  
   19.13  structure Numeral: NUMERAL =
   19.14 @@ -23,9 +23,8 @@
   19.15  fun mk_cnumeral 0 = @{cterm "Numeral.Pls"}
   19.16    | mk_cnumeral ~1 = @{cterm "Numeral.Min"}
   19.17    | mk_cnumeral i =
   19.18 -      let val (q, r) = Integer.divmod i 2 in
   19.19 -        Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q))
   19.20 -          (mk_cbit (Integer.machine_int r))
   19.21 +      let val (q, r) = Integer.div_mod i 2 in
   19.22 +        Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r)
   19.23        end;
   19.24  
   19.25  
    20.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Sep 18 11:06:22 2007 +0200
    20.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Sep 18 16:08:00 2007 +0200
    20.3 @@ -23,7 +23,7 @@
    20.4      fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b;
    20.5      fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
    20.6        | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min})
    20.7 -      | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
    20.8 +      | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
    20.9    in mk value end;
   20.10  
   20.11  in
   20.12 @@ -54,7 +54,7 @@
   20.13    | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
   20.14  
   20.15  fun int_of [] = 0
   20.16 -  | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
   20.17 +  | int_of (b :: bs) = b + 2 * int_of bs;
   20.18  
   20.19  fun dest_bin_str tm =
   20.20    let
   20.21 @@ -64,7 +64,7 @@
   20.22          ~1 :: bs => ("-", leading 1 bs)
   20.23        | bs => ("", leading 0 bs));
   20.24      val i = int_of rev_digs;
   20.25 -    val num = IntInf.toString (IntInf.abs i);
   20.26 +    val num = string_of_int (abs i);
   20.27    in
   20.28      if (i = 0 orelse i = 1) andalso z = 0 then raise Match
   20.29      else sign ^ implode (replicate z "0") ^ num
    21.1 --- a/src/HOL/ex/Binary.thy	Tue Sep 18 11:06:22 2007 +0200
    21.2 +++ b/src/HOL/ex/Binary.thy	Tue Sep 18 16:08:00 2007 +0200
    21.3 @@ -29,8 +29,7 @@
    21.4  
    21.5    fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0
    21.6      | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1
    21.7 -    | dest_binary (Const ("Binary.bit", _) $ bs $ b) =
    21.8 -        2 * dest_binary bs + IntInf.fromInt (dest_bit b)
    21.9 +    | dest_binary (Const ("Binary.bit", _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
   21.10      | dest_binary t = raise TERM ("dest_binary", [t]);
   21.11  
   21.12    fun mk_bit 0 = @{term False}
   21.13 @@ -42,8 +41,8 @@
   21.14      | mk_binary n =
   21.15          if n < 0 then raise TERM ("mk_binary", [])
   21.16          else
   21.17 -          let val (q, r) = IntInf.divMod (n, 2)
   21.18 -          in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
   21.19 +          let val (q, r) = Integer.div_mod n 2
   21.20 +          in @{term bit} $ mk_binary q $ mk_bit r end;
   21.21  end
   21.22  *}
   21.23  
   21.24 @@ -162,7 +161,7 @@
   21.25  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   21.26    if n = 0 then NONE
   21.27    else
   21.28 -    let val (k, l) = IntInf.divMod (m, n)
   21.29 +    let val (k, l) = Integer.div_mod m n
   21.30      in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
   21.31  
   21.32  end;
    22.1 --- a/src/HOL/ex/Random.thy	Tue Sep 18 11:06:22 2007 +0200
    22.2 +++ b/src/HOL/ex/Random.thy	Tue Sep 18 16:08:00 2007 +0200
    22.3 @@ -131,30 +131,27 @@
    22.4  ML {*
    22.5  signature RANDOM =
    22.6  sig
    22.7 -  type seed = IntInf.int;
    22.8 +  type seed = int;
    22.9    val seed: unit -> seed;
   22.10 -  val value: IntInf.int -> seed -> IntInf.int * seed;
   22.11 +  val value: int -> seed -> int * seed;
   22.12  end;
   22.13  
   22.14  structure Random : RANDOM =
   22.15  struct
   22.16  
   22.17 -open IntInf;
   22.18 -
   22.19  exception RANDOM;
   22.20  
   22.21  type seed = int;
   22.22  
   22.23  local
   22.24 -  val a = fromInt 16807;
   22.25 -    (*greetings to SML/NJ*)
   22.26 -  val m = (the o fromString) "2147483647";
   22.27 +  val a = 16807;
   22.28 +  val m = 2147483647;
   22.29  in
   22.30    fun next s = (a * s) mod m;
   22.31  end;
   22.32  
   22.33  local
   22.34 -  val seed_ref = ref (fromInt 1);
   22.35 +  val seed_ref = ref 1;
   22.36  in
   22.37    fun seed () = CRITICAL (fn () =>
   22.38      let
    23.1 --- a/src/HOL/ex/coopereif.ML	Tue Sep 18 11:06:22 2007 +0200
    23.2 +++ b/src/HOL/ex/coopereif.ML	Tue Sep 18 16:08:00 2007 +0200
    23.3 @@ -10,8 +10,6 @@
    23.4  
    23.5  open GeneratedCooper;
    23.6  
    23.7 -val nat = GeneratedCooper.nat o Integer.int;
    23.8 -
    23.9  fun i_of_term vs t = case t
   23.10   of Free(xn,xT) => (case AList.lookup (op aconv) vs t
   23.11     of NONE   => error "Variable not found in the list!"
    24.1 --- a/src/HOL/ex/reflection.ML	Tue Sep 18 11:06:22 2007 +0200
    24.2 +++ b/src/HOL/ex/reflection.ML	Tue Sep 18 16:08:00 2007 +0200
    24.3 @@ -200,7 +200,7 @@
    24.4     val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*)
    24.5     val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) => 
    24.6                            (cert n, snd (valOf (AList.lookup (op =) tml xn0)) 
    24.7 -                             |> (index_of #> IntInf.fromInt #> HOLogic.mk_nat #> cert))) 
    24.8 +                             |> (index_of #> HOLogic.mk_nat #> cert))) 
    24.9                        subst
   24.10     val subst_vs = 
   24.11      let 
    25.1 --- a/src/HOL/ex/svc_funcs.ML	Tue Sep 18 11:06:22 2007 +0200
    25.2 +++ b/src/HOL/ex/svc_funcs.ML	Tue Sep 18 16:08:00 2007 +0200
    25.3 @@ -27,12 +27,8 @@
    25.4     | UnInterp of string * expr list
    25.5     | FalseExpr
    25.6     | TrueExpr
    25.7 -   | Int of IntInf.int
    25.8 -   | Rat of IntInf.int * IntInf.int;
    25.9 -
   25.10 - fun signedInt i =
   25.11 -     if i < 0 then "-" ^ IntInf.toString (~i)
   25.12 -     else IntInf.toString i;
   25.13 +   | Int of int
   25.14 +   | Rat of int * int;
   25.15  
   25.16   fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
   25.17  
   25.18 @@ -49,8 +45,8 @@
   25.19               "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
   25.20             | ue (FalseExpr) = "FALSE "
   25.21             | ue (TrueExpr)  = "TRUE "
   25.22 -           | ue (Int i)     = (signedInt i) ^ " "
   25.23 -           | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
   25.24 +           | ue (Int i)     = signed_string_of_int i ^ " "
   25.25 +           | ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int j ^ " "
   25.26       in
   25.27           ue t
   25.28       end;
    26.1 --- a/src/HOL/hologic.ML	Tue Sep 18 11:06:22 2007 +0200
    26.2 +++ b/src/HOL/hologic.ML	Tue Sep 18 16:08:00 2007 +0200
    26.3 @@ -82,8 +82,8 @@
    26.4    val mk_Suc: term -> term
    26.5    val dest_Suc: term -> term
    26.6    val Suc_zero: term
    26.7 -  val mk_nat: integer -> term
    26.8 -  val dest_nat: term -> integer
    26.9 +  val mk_nat: int -> term
   26.10 +  val dest_nat: term -> int
   26.11    val class_size: string
   26.12    val size_const: typ -> term
   26.13    val bitT: typ
   26.14 @@ -95,12 +95,12 @@
   26.15    val pls_const: term
   26.16    val min_const: term
   26.17    val bit_const: term
   26.18 -  val mk_numeral: integer -> term
   26.19 -  val dest_numeral: term -> integer
   26.20 +  val mk_numeral: int -> term
   26.21 +  val dest_numeral: term -> int
   26.22    val number_of_const: typ -> term
   26.23    val add_numerals: term -> (term * typ) list -> (term * typ) list
   26.24 -  val mk_number: typ -> integer -> term
   26.25 -  val dest_number: term -> typ * integer
   26.26 +  val mk_number: typ -> int -> term
   26.27 +  val dest_number: term -> typ * int
   26.28    val realT: typ
   26.29    val nibbleT: typ
   26.30    val mk_nibble: int -> term
   26.31 @@ -423,13 +423,13 @@
   26.32  
   26.33  val Suc_zero = mk_Suc zero;
   26.34  
   26.35 -fun mk_nat (n: integer) =
   26.36 +fun mk_nat n =
   26.37    let
   26.38      fun mk 0 = zero
   26.39        | mk n = mk_Suc (mk (n - 1));
   26.40    in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
   26.41  
   26.42 -fun dest_nat (Const ("HOL.zero_class.zero", _)) = (0: integer)
   26.43 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
   26.44    | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   26.45    | dest_nat t = raise TERM ("dest_nat", [t]);
   26.46  
   26.47 @@ -465,13 +465,12 @@
   26.48  fun mk_numeral 0 = pls_const
   26.49    | mk_numeral ~1 = min_const
   26.50    | mk_numeral i =
   26.51 -      let val (q, r) = Integer.divmod i 2
   26.52 -      in bit_const $ mk_numeral q $ mk_bit (Integer.machine_int r) end;
   26.53 +      let val (q, r) = Integer.div_mod i 2;
   26.54 +      in bit_const $ mk_numeral q $ mk_bit r end;
   26.55  
   26.56  fun dest_numeral (Const ("Numeral.Pls", _)) = 0
   26.57    | dest_numeral (Const ("Numeral.Min", _)) = ~1
   26.58 -  | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
   26.59 -      2 * dest_numeral bs + Integer.int (dest_bit b)
   26.60 +  | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
   26.61    | dest_numeral t = raise TERM ("dest_numeral", [t]);
   26.62  
   26.63  fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
    27.1 --- a/src/HOL/int_arith1.ML	Tue Sep 18 11:06:22 2007 +0200
    27.2 +++ b/src/HOL/int_arith1.ML	Tue Sep 18 16:08:00 2007 +0200
    27.3 @@ -147,9 +147,9 @@
    27.4  (*Order integers by absolute value and then by sign. The standard integer
    27.5    ordering is not well-founded.*)
    27.6  fun num_ord (i,j) =
    27.7 -      (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
    27.8 -            EQUAL => int_ord (IntInf.sign i, IntInf.sign j) 
    27.9 -          | ord => ord);
   27.10 +  (case int_ord (abs i, abs j) of
   27.11 +    EQUAL => int_ord (Int.sign i, Int.sign j) 
   27.12 +  | ord => ord);
   27.13  
   27.14  (*This resembles Term.term_ord, but it puts binary numerals before other
   27.15    non-atomic terms.*)
   27.16 @@ -265,11 +265,11 @@
   27.17  
   27.18  (*Fractions as pairs of ints. Can't use Rat.rat because the representation
   27.19    needs to preserve negative values in the denominator.*)
   27.20 -fun mk_frac (p, q : IntInf.int) = if q = 0 then raise Div else (p, q);
   27.21 +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
   27.22  
   27.23  (*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   27.24    Fractions are reduced later by the cancel_numeral_factor simproc.*)
   27.25 -fun add_frac ((p1 : IntInf.int, q1 : IntInf.int), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   27.26 +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   27.27  
   27.28  val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
   27.29  
   27.30 @@ -421,9 +421,9 @@
   27.31  
   27.32  structure CombineNumeralsData =
   27.33    struct
   27.34 -  type coeff            = IntInf.int
   27.35 -  val iszero            = (fn x : IntInf.int => x = 0)
   27.36 -  val add               = IntInf.+
   27.37 +  type coeff            = int
   27.38 +  val iszero            = (fn x => x = 0)
   27.39 +  val add               = op +
   27.40    val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   27.41    val dest_sum          = dest_sum
   27.42    val mk_coeff          = mk_coeff
   27.43 @@ -451,8 +451,8 @@
   27.44  (*Version for fields, where coefficients can be fractions*)
   27.45  structure FieldCombineNumeralsData =
   27.46    struct
   27.47 -  type coeff            = IntInf.int * IntInf.int
   27.48 -  val iszero            = (fn (p : IntInf.int, q) => p = 0)
   27.49 +  type coeff            = int * int
   27.50 +  val iszero            = (fn (p, q) => p = 0)
   27.51    val add               = add_frac
   27.52    val mk_sum            = long_mk_sum
   27.53    val dest_sum          = dest_sum
    28.1 --- a/src/HOL/nat_simprocs.ML	Tue Sep 18 11:06:22 2007 +0200
    28.2 +++ b/src/HOL/nat_simprocs.ML	Tue Sep 18 16:08:00 2007 +0200
    28.3 @@ -20,7 +20,7 @@
    28.4  (*Utilities*)
    28.5  
    28.6  fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
    28.7 -fun dest_number t = IntInf.max (0, snd (HOLogic.dest_number t));
    28.8 +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    28.9  
   28.10  fun find_first_numeral past (t::terms) =
   28.11          ((dest_number t, t, rev past @ terms)
   28.12 @@ -119,7 +119,7 @@
   28.13    in
   28.14       if relaxed orelse exists prod_has_numeral ts then 
   28.15         if k=0 then ts
   28.16 -       else mk_number (IntInf.fromInt k) :: ts
   28.17 +       else mk_number k :: ts
   28.18       else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
   28.19    end;
   28.20  
   28.21 @@ -234,9 +234,9 @@
   28.22  
   28.23  structure CombineNumeralsData =
   28.24    struct
   28.25 -  type coeff            = IntInf.int
   28.26 -  val iszero            = (fn x : IntInf.int => x = 0)
   28.27 -  val add               = IntInf.+
   28.28 +  type coeff            = int
   28.29 +  val iszero            = (fn x => x = 0)
   28.30 +  val add               = op +
   28.31    val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   28.32    val dest_sum          = dest_Sucs_sum false
   28.33    val mk_coeff          = mk_coeff
    29.1 --- a/src/Provers/Arith/cancel_factor.ML	Tue Sep 18 11:06:22 2007 +0200
    29.2 +++ b/src/Provers/Arith/cancel_factor.ML	Tue Sep 18 16:08:00 2007 +0200
    29.3 @@ -60,12 +60,11 @@
    29.4              val d = 0
    29.5                |> fold (Integer.gcd o snd) tks
    29.6                |> fold (Integer.gcd o snd) uks;
    29.7 -            val d' = Integer.machine_int d;
    29.8            in
    29.9              if d = 0 orelse d = 1 then NONE
   29.10              else SOME
   29.11                (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss)
   29.12 -                (t, Data.mk_bal (div_sum d' tks, div_sum d' uks)))
   29.13 +                (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
   29.14            end));
   29.15  
   29.16  
    30.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Tue Sep 18 11:06:22 2007 +0200
    30.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Tue Sep 18 16:08:00 2007 +0200
    30.3 @@ -22,8 +22,8 @@
    30.4    (*abstract syntax*)
    30.5    val mk_bal: term * term -> term
    30.6    val dest_bal: term -> term * term
    30.7 -  val mk_coeff: IntInf.int * term -> term
    30.8 -  val dest_coeff: term -> IntInf.int * term
    30.9 +  val mk_coeff: int * term -> term
   30.10 +  val dest_coeff: term -> int * term
   30.11    (*rules*)
   30.12    val cancel: thm
   30.13    val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
    31.1 --- a/src/Provers/Arith/cancel_numerals.ML	Tue Sep 18 11:06:22 2007 +0200
    31.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Tue Sep 18 16:08:00 2007 +0200
    31.3 @@ -29,9 +29,9 @@
    31.4    val dest_sum: term -> term list
    31.5    val mk_bal: term * term -> term
    31.6    val dest_bal: term -> term * term
    31.7 -  val mk_coeff: IntInf.int * term -> term
    31.8 -  val dest_coeff: term -> IntInf.int * term
    31.9 -  val find_first_coeff: term -> term list -> IntInf.int * term list
   31.10 +  val mk_coeff: int * term -> term
   31.11 +  val dest_coeff: term -> int * term
   31.12 +  val find_first_coeff: term -> term list -> int * term list
   31.13    (*rules*)
   31.14    val bal_add1: thm
   31.15    val bal_add2: thm
    32.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 18 11:06:22 2007 +0200
    32.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 18 16:08:00 2007 +0200
    32.3 @@ -58,7 +58,7 @@
    32.4  
    32.5    (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
    32.6    val pre_tac: Proof.context -> int -> tactic
    32.7 -  val number_of: IntInf.int * typ -> term
    32.8 +  val number_of: int * typ -> term
    32.9  
   32.10    (*the limit on the number of ~= allowed; because each ~= is split
   32.11      into two cases, this can lead to an explosion*)
   32.12 @@ -154,11 +154,11 @@
   32.13                  | NotLessD of injust
   32.14                  | NotLeD of injust
   32.15                  | NotLeDD of injust
   32.16 -                | Multiplied of IntInf.int * injust
   32.17 -                | Multiplied2 of IntInf.int * injust
   32.18 +                | Multiplied of int * injust
   32.19 +                | Multiplied2 of int * injust
   32.20                  | Added of injust * injust;
   32.21  
   32.22 -datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust;
   32.23 +datatype lineq = Lineq of int * lineq_type * int list * injust;
   32.24  
   32.25  (* ------------------------------------------------------------------------- *)
   32.26  (* Finding a (counter) example from the trace of a failed elimination        *)
   32.27 @@ -178,7 +178,7 @@
   32.28    | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
   32.29  
   32.30  (* PRE: ex[v] must be 0! *)
   32.31 -fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) =
   32.32 +fun eval ex v (a, le, cs) =
   32.33    let
   32.34      val rs = map Rat.rat_of_int cs;
   32.35      val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
   32.36 @@ -332,9 +332,9 @@
   32.37  fun is_answer (ans as Lineq(k,ty,l,_)) =
   32.38    case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
   32.39  
   32.40 -fun calc_blowup (l:IntInf.int list) =
   32.41 +fun calc_blowup l =
   32.42    let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
   32.43 -  in (length p) * (length n) end;
   32.44 +  in length p * length n end;
   32.45  
   32.46  (* ------------------------------------------------------------------------- *)
   32.47  (* Main elimination code:                                                    *)
   32.48 @@ -360,9 +360,9 @@
   32.49  fun print_ineqs ineqs =
   32.50    if !trace then
   32.51       tracing(cat_lines(""::map (fn Lineq(c,t,l,_) =>
   32.52 -       IntInf.toString c ^
   32.53 +       string_of_int c ^
   32.54         (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
   32.55 -       commas(map IntInf.toString l)) ineqs))
   32.56 +       commas(map string_of_int l)) ineqs))
   32.57    else ();
   32.58  
   32.59  type history = (int * lineq list) list;
   32.60 @@ -381,7 +381,7 @@
   32.61    let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
   32.62    if not (null eqs) then
   32.63       let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
   32.64 -         val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
   32.65 +         val sclist = sort (fn (x,y) => int_ord (abs x, abs y))
   32.66                             (List.filter (fn i => i<>0) clist)
   32.67           val c = hd sclist
   32.68           val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
   32.69 @@ -487,8 +487,8 @@
   32.70          | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   32.71          | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
   32.72          | mk (Added (j1, j2))     = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
   32.73 -        | mk (Multiplied (n, j))  = (trace_msg ("*" ^ IntInf.toString n); trace_thm "*" (multn (n, mk j)))
   32.74 -        | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ IntInf.toString n); trace_thm "**" (multn2 (n, mk j)))
   32.75 +        | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
   32.76 +        | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
   32.77  
   32.78    in trace_msg "mkthm";
   32.79       let val thm = trace_thm "Final thm:" (mk just)
   32.80 @@ -507,13 +507,11 @@
   32.81  end;
   32.82  
   32.83  fun coeff poly atom =
   32.84 -  AList.lookup (op aconv) poly atom |> the_default (0: integer);
   32.85 -
   32.86 -fun lcms ks = fold Integer.lcm ks 1;
   32.87 +  AList.lookup (op aconv) poly atom |> the_default 0;
   32.88  
   32.89  fun integ(rlhs,r,rel,rrhs,s,d) =
   32.90  let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
   32.91 -    val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
   32.92 +    val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
   32.93      fun mult(t,r) =
   32.94          let val (i,j) = Rat.quotient_of_rat r
   32.95          in (t,i * (m div j)) end
   32.96 @@ -547,9 +545,9 @@
   32.97  
   32.98  fun print_atom((a,d),r) =
   32.99    let val (p,q) = Rat.quotient_of_rat r
  32.100 -      val s = if d then IntInf.toString p else
  32.101 +      val s = if d then string_of_int p else
  32.102                if p = 0 then "0"
  32.103 -              else IntInf.toString p ^ "/" ^ IntInf.toString q
  32.104 +              else string_of_int p ^ "/" ^ string_of_int q
  32.105    in a ^ " = " ^ s end;
  32.106  
  32.107  fun produce_ex sds =
    33.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Sep 18 11:06:22 2007 +0200
    33.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 18 16:08:00 2007 +0200
    33.3 @@ -29,7 +29,7 @@
    33.4    val var: indexname -> term
    33.5    val read_nat: string -> int option
    33.6    val read_int: string -> int option
    33.7 -  val read_xnum: string -> {radix: int, leading_zeros: int, value: IntInf.int}
    33.8 +  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
    33.9    val read_idents: string -> string list
   33.10    val fixedN: string
   33.11    val constN: string
   33.12 @@ -402,7 +402,7 @@
   33.13        | "0" :: "b" :: cs => (1, 2, cs)
   33.14        | "-" :: cs => (~1, 10, cs)
   33.15        | cs => (1, 10, cs));
   33.16 -    val value = IntInf.fromInt sign * #1 (Library.read_intinf radix digs);
   33.17 +    val value = sign * #1 (Library.read_radix_int radix digs);
   33.18    in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
   33.19  
   33.20  end;
    34.1 --- a/src/Pure/library.ML	Tue Sep 18 11:06:22 2007 +0200
    34.2 +++ b/src/Pure/library.ML	Tue Sep 18 16:08:00 2007 +0200
    34.3 @@ -125,7 +125,7 @@
    34.4    val string_of_int: int -> string
    34.5    val signed_string_of_int: int -> string
    34.6    val string_of_indexname: string * int -> string
    34.7 -  val read_intinf: int -> string list -> IntInf.int * string list
    34.8 +  val read_radix_int: int -> string list -> int * string list
    34.9    val read_int: string list -> int * string list
   34.10    val oct_char: string -> string
   34.11  
   34.12 @@ -640,20 +640,20 @@
   34.13  
   34.14  (* read integers *)
   34.15  
   34.16 -fun read_intinf radix cs =
   34.17 +fun read_radix_int radix cs =
   34.18    let
   34.19      val zero = ord "0";
   34.20      val limit = zero + radix;
   34.21      fun scan (num, []) = (num, [])
   34.22        | scan (num, c :: cs) =
   34.23          if zero <= ord c andalso ord c < limit then
   34.24 -          scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs)
   34.25 +          scan (radix * num + (ord c - zero), cs)
   34.26          else (num, c :: cs);
   34.27 -  in scan (IntInf.fromInt 0, cs) end;
   34.28 +  in scan (0, cs) end;
   34.29  
   34.30 -fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs);
   34.31 +val read_int = read_radix_int 10;
   34.32  
   34.33 -fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s))));
   34.34 +fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
   34.35  
   34.36  
   34.37  
    35.1 --- a/src/Tools/code/code_target.ML	Tue Sep 18 11:06:22 2007 +0200
    35.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 18 16:08:00 2007 +0200
    35.3 @@ -236,12 +236,12 @@
    35.4            else if c = c_bit1 then SOME 1
    35.5            else NONE
    35.6        | dest_bit _ = NONE;
    35.7 -    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME (IntInf.fromInt 0)
    35.8 -          else if c = c_min then SOME (IntInf.fromInt ~1)
    35.9 +    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
   35.10 +          else if c = c_min then SOME ~1
   35.11            else NONE
   35.12        | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
   35.13            if c = c_bit then case (dest_numeral t1, dest_bit t2)
   35.14 -           of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b)
   35.15 +           of (SOME n, SOME b) => SOME (2 * n + b)
   35.16              | _ => NONE
   35.17            else NONE
   35.18        | dest_numeral _ = NONE;
   35.19 @@ -1631,15 +1631,15 @@
   35.20  val pretty : (string * {
   35.21      pretty_char: string -> string,
   35.22      pretty_string: string -> string,
   35.23 -    pretty_numeral: bool -> IntInf.int -> string,
   35.24 +    pretty_numeral: bool -> int -> string,
   35.25      pretty_list: Pretty.T list -> Pretty.T,
   35.26      infix_cons: int * string
   35.27    }) list = [
   35.28    ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
   35.29        pretty_string = ML_Syntax.print_string,
   35.30        pretty_numeral = fn unbounded => fn k =>
   35.31 -        if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)"
   35.32 -        else IntInf.toString k,
   35.33 +        if unbounded then "(" ^ string_of_int k ^ " : int)"
   35.34 +        else string_of_int k,
   35.35        pretty_list = Pretty.enum "," "[" "]",
   35.36        infix_cons = (7, "::")}),
   35.37    ("OCaml", { pretty_char = fn c => enclose "'" "'"
   35.38 @@ -1649,15 +1649,15 @@
   35.39              else c
   35.40            end),
   35.41        pretty_string = (fn _ => error "OCaml: no pretty strings"),
   35.42 -      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
   35.43 +      pretty_numeral = fn unbounded => fn k => if k >= 0 then
   35.44              if unbounded then
   35.45 -              "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
   35.46 -            else IntInf.toString k
   35.47 +              "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   35.48 +            else string_of_int k
   35.49            else
   35.50              if unbounded then
   35.51                "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
   35.52 -                o IntInf.toString o op ~) k ^ ")"
   35.53 -            else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k,
   35.54 +                o string_of_int o op ~) k ^ ")"
   35.55 +            else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
   35.56        pretty_list = Pretty.enum ";" "[" "]",
   35.57        infix_cons = (6, "::")}),
   35.58    ("Haskell", { pretty_char = fn c => enclose "'" "'"
   35.59 @@ -1667,10 +1667,8 @@
   35.60              else c
   35.61            end),
   35.62        pretty_string = ML_Syntax.print_string,
   35.63 -      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
   35.64 -            IntInf.toString k
   35.65 -          else
   35.66 -            (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
   35.67 +      pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
   35.68 +          else enclose "(" ")" (signed_string_of_int k),
   35.69        pretty_list = Pretty.enum "," "[" "]",
   35.70        infix_cons = (5, ":")})
   35.71  ];
    36.1 --- a/src/Tools/float.ML	Tue Sep 18 11:06:22 2007 +0200
    36.2 +++ b/src/Tools/float.ML	Tue Sep 18 16:08:00 2007 +0200
    36.3 @@ -7,7 +7,7 @@
    36.4  
    36.5  signature FLOAT =
    36.6  sig
    36.7 -  type float = integer * integer
    36.8 +  type float = int * int
    36.9    val zero: float
   36.10    val eq: float * float -> bool
   36.11    val ord: float * float -> order
   36.12 @@ -25,25 +25,25 @@
   36.13  structure Float : FLOAT =
   36.14  struct
   36.15  
   36.16 -type float = integer * integer;
   36.17 +type float = int * int;
   36.18  
   36.19  val zero: float = (0, 0);
   36.20  
   36.21  fun add (a1, b1) (a2, b2) =
   36.22 -  if Integer.ord (b1, b2) = LESS then
   36.23 -    (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
   36.24 +  if b1 < b2 then
   36.25 +    (a1 + a2 * Integer.square (b2 - b1), b1)
   36.26    else
   36.27 -    (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
   36.28 +    (a1 * Integer.square (b1 - b2) + a2, b2);
   36.29  
   36.30  fun sub (a1, b1) (a2, b2) =
   36.31 -  if Integer.ord (b1, b2) = LESS then
   36.32 -    (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
   36.33 +  if b1 < b2 then
   36.34 +    (a1 - a2 * Integer.square (b2 - b1), b1)
   36.35    else
   36.36 -    (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
   36.37 +    (a1 * Integer.square (b1 - b2) - a2, b2);
   36.38  
   36.39 -fun neg (a, b) = (Integer.neg a, b);
   36.40 +fun neg (a, b) = (~ a, b);
   36.41  
   36.42 -fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
   36.43 +fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2);
   36.44  
   36.45  fun sign (a, b) = Integer.sign a;
   36.46  
   36.47 @@ -54,7 +54,7 @@
   36.48  fun min r s = case ord (r, s) of LESS => r | _ => s;
   36.49  fun max r s = case ord (r, s) of LESS => s | _ => r;
   36.50  
   36.51 -fun positive_part (a, b) = (Integer.max 0 a, b);
   36.52 -fun negative_part (a, b) = (Integer.min 0 a, b);
   36.53 +fun positive_part (a, b) = (Int.max (0, a), b);
   36.54 +fun negative_part (a, b) = (Int.min (0, a), b);
   36.55  
   36.56  end;
    37.1 --- a/src/Tools/integer.ML	Tue Sep 18 11:06:22 2007 +0200
    37.2 +++ b/src/Tools/integer.ML	Tue Sep 18 16:08:00 2007 +0200
    37.3 @@ -7,73 +7,27 @@
    37.4  
    37.5  signature INTEGER =
    37.6  sig
    37.7 -  eqtype int
    37.8 -  val zero: int
    37.9 -  val one: int
   37.10 -  val two: int
   37.11 -  val int: Int.int -> int
   37.12 -  val machine_int: int -> Int.int
   37.13 -  val string_of_int: int -> string
   37.14 -  val int_of_string: string -> int option
   37.15 -  val eq: int * int -> bool
   37.16 -  val ord: int * int -> order
   37.17 -  val le: int -> int -> bool
   37.18 -  val lt: int -> int -> bool
   37.19 -  val signabs: int -> order * int
   37.20    val sign: int -> order
   37.21 -  val abs: int -> int
   37.22 -  val min: int -> int -> int
   37.23 -  val max: int -> int -> int
   37.24 -  val inc: int -> int
   37.25 -  val add: int -> int -> int
   37.26 -  val sub: int -> int -> int
   37.27 -  val mult: int -> int -> int
   37.28 -  val divmod: int -> int -> int * int
   37.29 -  val div: int -> int -> int
   37.30 -  val mod: int -> int -> int
   37.31 -  val neg: int -> int
   37.32 -  val exp: int -> int
   37.33 -  val log: int -> int
   37.34 +  val sum: int list -> int
   37.35 +  val div_mod: int -> int -> int * int
   37.36 +  val square: int -> int
   37.37    val pow: int -> int -> int (* exponent -> base -> result *)
   37.38    val gcd: int -> int -> int
   37.39 +  val gcds: int list -> int
   37.40    val lcm: int -> int -> int
   37.41 +  val lcms: int list -> int
   37.42  end;
   37.43  
   37.44  structure Integer : INTEGER =
   37.45  struct
   37.46  
   37.47 -open IntInf;
   37.48 -
   37.49 -val int = fromInt;
   37.50 +fun sign x = int_ord (x, 0);
   37.51  
   37.52 -val zero = int 0;
   37.53 -val one = int 1;
   37.54 -val two = int 2;
   37.55 -
   37.56 -val machine_int = toInt;
   37.57 -val string_of_int = toString;
   37.58 -val int_of_string = fromString;
   37.59 +fun sum xs = fold (curry op +) xs 0;
   37.60  
   37.61 -val eq = op = : int * int -> bool;
   37.62 -val ord = compare;
   37.63 -val le = curry (op <=);
   37.64 -val lt = curry (op <);
   37.65 -
   37.66 -fun sign k = ord (k, zero);
   37.67 -fun signabs k = (ord (k, zero), abs k);
   37.68 +fun div_mod x y = IntInf.divMod (x, y);
   37.69  
   37.70 -val min = curry min;
   37.71 -val max = curry max;
   37.72 -
   37.73 -val inc = curry (op +) one;
   37.74 -
   37.75 -val add = curry (op +);
   37.76 -val sub = curry (op -);
   37.77 -val mult = curry ( op * );
   37.78 -val divmod = curry divMod;
   37.79 -nonfix div val div = curry div;
   37.80 -nonfix mod val mod = curry mod;
   37.81 -val neg = ~;
   37.82 +fun square x = x * x;
   37.83  
   37.84  fun pow k l =
   37.85    let
   37.86 @@ -81,38 +35,24 @@
   37.87        | pw 1 l = l
   37.88        | pw k l =
   37.89            let
   37.90 -            val (k', r) = divmod k 2;
   37.91 -            val l' = pw k' (mult l l);
   37.92 -          in if r = 0 then l' else mult l' l end;
   37.93 -  in if k < zero
   37.94 +            val (k', r) = div_mod k 2;
   37.95 +            val l' = pw k' (l * l);
   37.96 +          in if r = 0 then l' else l' * l end;
   37.97 +  in
   37.98 +    if k < 0
   37.99      then error "pow: negative exponent"
  37.100      else pw k l
  37.101    end;
  37.102  
  37.103 -fun exp k = pow k two;
  37.104 -val log = int o log2;
  37.105 -
  37.106  fun gcd x y =
  37.107    let
  37.108 -    fun gxd x y = if y = zero then x else gxd y (mod x y)
  37.109 -  in if lt x y then gxd y x else gxd x y end;
  37.110 +    fun gxd x y = if y = 0 then x else gxd y (x mod y)
  37.111 +  in if x < y then gxd y x else gxd x y end;
  37.112  
  37.113 -fun lcm x y = div (mult x y) (gcd x y);
  37.114 +fun gcds xs = fold gcd xs 0;
  37.115 +
  37.116 +fun lcm x y = (x * y) div (gcd x y);
  37.117 +fun lcms xs = fold lcm xs 1;
  37.118  
  37.119  end;
  37.120  
  37.121 -type integer = Integer.int;
  37.122 -
  37.123 -infix 7 *%;
  37.124 -infix 6 +% -%;
  37.125 -infix 4 =% <% <=% >% >=% <>%;
  37.126 -
  37.127 -fun a +% b = Integer.add a b;
  37.128 -fun a -% b = Integer.sub a b;
  37.129 -fun a *% b = Integer.mult a b;
  37.130 -fun a =% b = Integer.eq (a, b);
  37.131 -fun a <% b = Integer.lt a b;
  37.132 -fun a <=% b = Integer.le a b;
  37.133 -fun a >% b = b <% a;
  37.134 -fun a >=% b = b <=% a;
  37.135 -fun a <>% b = not (a =% b);
    38.1 --- a/src/Tools/rat.ML	Tue Sep 18 11:06:22 2007 +0200
    38.2 +++ b/src/Tools/rat.ML	Tue Sep 18 16:08:00 2007 +0200
    38.3 @@ -12,15 +12,14 @@
    38.4    val zero: rat
    38.5    val one: rat
    38.6    val two: rat
    38.7 -  val rat_of_int: integer -> rat
    38.8 -  val rat_of_quotient: integer * integer -> rat
    38.9 -  val quotient_of_rat: rat -> integer * integer
   38.10 +  val rat_of_int: int -> rat
   38.11 +  val rat_of_quotient: int * int -> rat
   38.12 +  val quotient_of_rat: rat -> int * int
   38.13    val string_of_rat: rat -> string
   38.14    val eq: rat * rat -> bool
   38.15    val ord: rat * rat -> order
   38.16    val le: rat -> rat -> bool
   38.17    val lt: rat -> rat -> bool
   38.18 -  val signabs: rat -> order * rat
   38.19    val sign: rat -> order
   38.20    val abs: rat -> rat
   38.21    val add: rat -> rat -> rat
   38.22 @@ -37,16 +36,16 @@
   38.23  fun common (p1, q1) (p2, q2) =
   38.24    let
   38.25      val m = Integer.lcm q1 q2;
   38.26 -  in ((Integer.mult p1 (Integer.div m q1), Integer.mult p2 (Integer.div m q2)), m) end;
   38.27 +  in ((p1 * (m div q1), p2 * (m div q2)), m) end;
   38.28  
   38.29 -datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *)
   38.30 +datatype rat = Rat of int * int;  (*nominator, denominator (positive!)*)
   38.31  
   38.32  exception DIVZERO;
   38.33  
   38.34  fun rat_of_quotient (p, q) =
   38.35    let
   38.36 -    val m = Integer.gcd (Integer.abs p) q
   38.37 -  in Rat (Integer.div p m, Integer.div q m) end handle Div => raise DIVZERO;
   38.38 +    val m = Integer.gcd (Int.abs p) q
   38.39 +  in Rat (p div m, q div m) end handle Div => raise DIVZERO;
   38.40  
   38.41  fun quotient_of_rat (Rat r) = r;
   38.42  
   38.43 @@ -57,11 +56,12 @@
   38.44  val two = rat_of_int 2;
   38.45  
   38.46  fun string_of_rat (Rat (p, q)) =
   38.47 -  Integer.string_of_int p ^ "/" ^ Integer.string_of_int q;
   38.48 +  string_of_int p ^ "/" ^ string_of_int q;
   38.49  
   38.50  fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
   38.51  
   38.52 -fun ord (Rat (p1, q1), Rat (p2, q2)) = case (Integer.sign p1, Integer.sign p2)
   38.53 +fun ord (Rat (p1, q1), Rat (p2, q2)) =
   38.54 + case (Integer.sign p1, Integer.sign p2)
   38.55   of (LESS, EQUAL) => LESS
   38.56    | (LESS, GREATER) => LESS
   38.57    | (EQUAL, LESS) => GREATER
   38.58 @@ -69,38 +69,35 @@
   38.59    | (EQUAL, GREATER) => LESS
   38.60    | (GREATER, LESS) => GREATER
   38.61    | (GREATER, EQUAL) => GREATER
   38.62 -  | _ => Integer.ord (fst (common (p1, q1) (p2, q2)));
   38.63 +  | _ => int_ord (fst (common (p1, q1) (p2, q2)));
   38.64  
   38.65  fun le a b = not (ord (a, b) = GREATER);
   38.66  fun lt a b = (ord (a, b) = LESS);
   38.67  
   38.68  fun sign (Rat (p, _)) = Integer.sign p;
   38.69  
   38.70 -fun abs (Rat (p, q)) = Rat (Integer.abs p, q);
   38.71 -
   38.72 -fun signabs (Rat (p, q)) =
   38.73 -  let
   38.74 -    val (s, p') = Integer.signabs p;
   38.75 -  in (s, Rat (p', q)) end;
   38.76 +fun abs (Rat (p, q)) = Rat (Int.abs p, q);
   38.77  
   38.78  fun add (Rat (p1, q1)) (Rat (p2, q2)) =
   38.79    let
   38.80      val ((m1, m2), n) = common (p1, q1) (p2, q2);
   38.81 -  in rat_of_quotient (Integer.add m1 m2, n) end;
   38.82 +  in rat_of_quotient (m1 + m2, n) end;
   38.83  
   38.84  fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
   38.85 -  rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
   38.86 +  rat_of_quotient (p1 * p2, q1 * q2);
   38.87 +
   38.88 +fun neg (Rat (p, q)) = Rat (~ p, q);
   38.89  
   38.90 -fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
   38.91 -
   38.92 -fun inv (Rat (p, q)) = case Integer.sign p
   38.93 - of LESS => Rat (Integer.neg q, Integer.neg p)
   38.94 +fun inv (Rat (p, q)) =
   38.95 + case Integer.sign p
   38.96 + of LESS => Rat (~ q, ~ p)
   38.97    | EQUAL => raise DIVZERO
   38.98    | GREATER => Rat (q, p);
   38.99  
  38.100 -fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
  38.101 +fun rounddown (Rat (p, q)) = Rat (p div q, 1);
  38.102  
  38.103 -fun roundup (Rat (p, q)) = case Integer.divmod p q
  38.104 +fun roundup (Rat (p, q)) =
  38.105 + case Integer.div_mod p q
  38.106   of (m, 0) => Rat (m, 1)
  38.107    | (m, _) => Rat (m + 1, 1);
  38.108  
    39.1 --- a/src/ZF/Tools/numeral_syntax.ML	Tue Sep 18 11:06:22 2007 +0200
    39.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Tue Sep 18 16:08:00 2007 +0200
    39.3 @@ -8,8 +8,8 @@
    39.4  
    39.5  signature NUMERAL_SYNTAX =
    39.6  sig
    39.7 -  val dest_bin : term -> IntInf.int
    39.8 -  val mk_bin   : IntInf.int -> term
    39.9 +  val dest_bin : term -> int
   39.10 +  val mk_bin   : int -> term
   39.11    val int_tr   : term list -> term
   39.12    val int_tr'  : bool -> typ -> term list -> term
   39.13    val setup    : theory -> theory
   39.14 @@ -23,7 +23,7 @@
   39.15  val zero = Const("0", iT);
   39.16  val succ = Const("succ", iT --> iT);
   39.17  
   39.18 -fun mk_bit (0: IntInf.int) = zero
   39.19 +fun mk_bit 0 = zero
   39.20    | mk_bit 1 = succ$zero
   39.21    | mk_bit _ = sys_error "mk_bit";
   39.22  
   39.23 @@ -42,7 +42,7 @@
   39.24  and min_const = Const ("Bin.bin.Min", iT)
   39.25  and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
   39.26  
   39.27 -fun mk_bin (i: IntInf.int) =
   39.28 +fun mk_bin i =
   39.29    let fun bin_of_int 0  = []
   39.30    	    | bin_of_int ~1 = [~1]
   39.31      	| bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
   39.32 @@ -67,8 +67,8 @@
   39.33    | bin_of _ = raise Match;
   39.34  
   39.35  (*Convert a list of bits to an integer*)
   39.36 -fun integ_of [] = 0 : IntInf.int
   39.37 -  | integ_of (b :: bs) = (IntInf.fromInt b) + 2 * integ_of bs;
   39.38 +fun integ_of [] = 0
   39.39 +  | integ_of (b :: bs) = b + 2 * integ_of bs;
   39.40  
   39.41  val dest_bin = integ_of o bin_of;
   39.42  
   39.43 @@ -82,7 +82,7 @@
   39.44  	(case rev rev_digs of
   39.45  	     ~1 :: bs => ("-", prefix_len (equal 1) bs)
   39.46  	   | bs =>       ("",  prefix_len (equal 0) bs));
   39.47 -    val num = IntInf.toString (abs (integ_of rev_digs));
   39.48 +    val num = string_of_int (abs (integ_of rev_digs));
   39.49    in
   39.50      "#" ^ sign ^ implode (replicate zs "0") ^ num
   39.51    end;
    40.1 --- a/src/ZF/arith_data.ML	Tue Sep 18 11:06:22 2007 +0200
    40.2 +++ b/src/ZF/arith_data.ML	Tue Sep 18 16:08:00 2007 +0200
    40.3 @@ -100,13 +100,13 @@
    40.4        handle TERM _ => [t];
    40.5  
    40.6  (*Dummy version: the only arguments are 0 and 1*)
    40.7 -fun mk_coeff (0: IntInf.int, t) = zero
    40.8 +fun mk_coeff (0, t) = zero
    40.9    | mk_coeff (1, t) = t
   40.10    | mk_coeff _       = raise TERM("mk_coeff", []);
   40.11  
   40.12  (*Dummy version: the "coefficient" is always 1.
   40.13    In the result, the factors are sorted terms*)
   40.14 -fun dest_coeff t = (1 : IntInf.int, mk_prod (sort Term.term_ord (dest_prod t)));
   40.15 +fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
   40.16  
   40.17  (*Find first coefficient-term THAT MATCHES u*)
   40.18  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    41.1 --- a/src/ZF/int_arith.ML	Tue Sep 18 11:06:22 2007 +0200
    41.2 +++ b/src/ZF/int_arith.ML	Tue Sep 18 16:08:00 2007 +0200
    41.3 @@ -293,9 +293,9 @@
    41.4  
    41.5  structure CombineNumeralsData =
    41.6    struct
    41.7 -  type coeff            = IntInf.int
    41.8 -  val iszero            = (fn x : IntInf.int => x = 0)
    41.9 -  val add               = IntInf.+ 
   41.10 +  type coeff            = int
   41.11 +  val iszero            = (fn x => x = 0)
   41.12 +  val add               = op + 
   41.13    val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   41.14    val dest_sum          = dest_sum
   41.15    val mk_coeff          = mk_coeff
   41.16 @@ -333,9 +333,9 @@
   41.17  
   41.18  structure CombineNumeralsProdData =
   41.19    struct
   41.20 -  type coeff            = IntInf.int
   41.21 -  val iszero            = (fn x : IntInf.int => x = 0)
   41.22 -  val add               = IntInf.*
   41.23 +  type coeff            = int
   41.24 +  val iszero            = (fn x => x = 0)
   41.25 +  val add               = op *
   41.26    val mk_sum            = (fn T:typ => mk_prod)
   41.27    val dest_sum          = dest_prod
   41.28    fun mk_coeff(k,t) = if t=one then mk_numeral k