--- a/src/HOL/Integ/int_arith1.ML Thu Aug 10 11:27:34 2000 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu Aug 10 11:30:22 2000 +0200
@@ -266,6 +266,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 dest_sum = dest_sum
val mk_coeff = mk_coeff
--- a/src/HOL/Integ/nat_simprocs.ML Thu Aug 10 11:27:34 2000 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Aug 10 11:30:22 2000 +0200
@@ -254,6 +254,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 dest_sum = dest_Sucs_sum
val mk_coeff = mk_coeff
--- a/src/Provers/Arith/combine_numerals.ML Thu Aug 10 11:27:34 2000 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Thu Aug 10 11:30:22 2000 +0200
@@ -19,6 +19,7 @@
signature COMBINE_NUMERALS_DATA =
sig
(*abstract syntax*)
+ val add: int * int -> int (*addition (or multiplication) *)
val mk_sum: term list -> term
val dest_sum: term -> term list
val mk_coeff: int * term -> term
@@ -83,7 +84,7 @@
(Data.prove_conv
[Data.trans_tac reshape, rtac Data.left_distrib 1,
Data.numeral_simp_tac] sg
- (t', Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
+ (t', Data.mk_sum (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
handle TERM _ => None
| TYPE _ => None; (*Typically (if thy doesn't include Numeral)