# HG changeset patch
# User paulson
# Date 965899822 -7200
# Node ID c869d1886a32ea3fb1b0ca7bc52da564bd19c7e3
# Parent  e16e168984e1818ef756927035eec7d1d36543d2
new structure field "add" for CombineNumerals

diff -r e16e168984e1 -r c869d1886a32 src/HOL/Integ/int_arith1.ML
--- 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
diff -r e16e168984e1 -r c869d1886a32 src/HOL/Integ/nat_simprocs.ML
--- 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
diff -r e16e168984e1 -r c869d1886a32 src/Provers/Arith/combine_numerals.ML
--- 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)