src/ZF/Integ/int_arith.ML
changeset 9576 3df14e0a3a51
parent 9570 e16e168984e1
child 9648 35d761c7d934
--- a/src/ZF/Integ/int_arith.ML	Thu Aug 10 14:55:21 2000 +0200
+++ b/src/ZF/Integ/int_arith.ML	Fri Aug 11 10:34:02 2000 +0200
@@ -315,7 +315,7 @@
   
 val combine_numerals_prod = 
     prep_simproc ("int_combine_numerals_prod",
-		  prep_pats ["i $* j", "i $* j"],
+		  prep_pats ["i $* j"],
 		  CombineNumeralsProd.proc);
 
 end;