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