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