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