--- a/src/ZF/Integ/int_arith.ML Sat Feb 14 02:06:12 2004 +0100
+++ b/src/ZF/Integ/int_arith.ML Sun Feb 15 10:46:37 2004 +0100
@@ -219,7 +219,7 @@
structure CancelNumeralsCommon =
struct
- val mk_sum = mk_sum
+ val mk_sum = (fn T:typ => mk_sum)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -292,7 +292,7 @@
structure CombineNumeralsData =
struct
val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. #2*x $+ #3*x *)
+ val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -328,7 +328,7 @@
structure CombineNumeralsProdData =
struct
val add = op * : int*int -> int
- val mk_sum = mk_prod
+ val mk_sum = (fn T:typ => mk_prod)
val dest_sum = dest_prod
fun mk_coeff(k,t) = if t=one then mk_numeral k
else raise TERM("mk_coeff", [])