src/HOL/Integ/nat_simprocs.ML
changeset 23072 f64df9399329
parent 23058 c722004c5a22
--- 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