src/ZF/Integ/int_arith.ML
changeset 14387 e96d5c42c4b0
parent 13560 d9651081578b
child 15965 f422f8283491
--- 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", [])