# HG changeset patch
# User haftmann
# Date 1179837834 -7200
# Node ID f64df9399329c66b1a80952a14efe95672fbe090
# Parent  bf058e6405f88d8c0ae4ae8eac33ea04c96986b7
adjusted to change in Provers/Arith/combine_numerals.ML

diff -r bf058e6405f8 -r f64df9399329 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Tue May 22 13:55:30 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Tue May 22 14:43:54 2007 +0200
@@ -260,11 +260,11 @@
 
 (*Fractions as pairs of ints. Can't use Rat.rat because the representation
   needs to preserve negative values in the denominator.*)
-fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
+fun mk_frac (p, q : IntInf.int) = if q = 0 then raise Div else (p, q);
 
 (*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   Fractions are reduced later by the cancel_numeral_factor simproc.*)
-fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
+fun add_frac ((p1 : IntInf.int, q1 : IntInf.int), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
 
 val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
 
@@ -417,8 +417,8 @@
 structure CombineNumeralsData =
   struct
   type coeff            = IntInf.int
-  val iszero            = (fn x => x = 0)
-  val add               = IntInf.+ 
+  val iszero            = (fn x : IntInf.int => x = 0)
+  val add               = IntInf.+
   val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum          = dest_sum
   val mk_coeff          = mk_coeff
@@ -447,7 +447,7 @@
 structure FieldCombineNumeralsData =
   struct
   type coeff            = IntInf.int * IntInf.int
-  val iszero            = (fn (p, q) => p = 0)
+  val iszero            = (fn (p : IntInf.int, q) => p = 0)
   val add               = add_frac
   val mk_sum            = long_mk_sum
   val dest_sum          = dest_sum
diff -r bf058e6405f8 -r f64df9399329 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Tue May 22 13:55:30 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Tue May 22 14:43:54 2007 +0200
@@ -235,7 +235,7 @@
 structure CombineNumeralsData =
   struct
   type coeff            = IntInf.int
-  val iszero            = (fn x => x = 0)
+  val iszero            = (fn x : IntInf.int => x = 0)
   val add               = IntInf.+
   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   val dest_sum          = dest_Sucs_sum false
diff -r bf058e6405f8 -r f64df9399329 src/ZF/Integ/int_arith.ML
--- a/src/ZF/Integ/int_arith.ML	Tue May 22 13:55:30 2007 +0200
+++ b/src/ZF/Integ/int_arith.ML	Tue May 22 14:43:54 2007 +0200
@@ -294,7 +294,7 @@
 structure CombineNumeralsData =
   struct
   type coeff            = IntInf.int
-  val iszero            = (fn x => x = 0)
+  val iszero            = (fn x : IntInf.int => x = 0)
   val add               = IntInf.+ 
   val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   val dest_sum          = dest_sum
@@ -334,7 +334,7 @@
 structure CombineNumeralsProdData =
   struct
   type coeff            = IntInf.int
-  val iszero            = (fn x => x = 0)
+  val iszero            = (fn x : IntInf.int => x = 0)
   val add               = IntInf.*
   val mk_sum            = (fn T:typ => mk_prod)
   val dest_sum          = dest_prod