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;