changeset 17412 | e26cb20ef0cc |
parent 17223 | 430edc6b7826 |
child 20044 | 92cc2f4c7335 |
--- a/src/Provers/Arith/cancel_numerals.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Thu Sep 15 17:16:56 2005 +0200 @@ -54,7 +54,7 @@ (*For t = #n*u then put u in the table*) fun update_by_coeff t = - Termtab.curried_update (#2 (Data.dest_coeff t), ()); + Termtab.update (#2 (Data.dest_coeff t), ()); (*a left-to-right scan of terms1, seeking a term of the form #n*u, where #m*u is in terms2 for some m*)