--- a/src/Provers/Arith/combine_numerals.ML Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Thu Sep 01 22:15:12 2005 +0200
@@ -57,9 +57,9 @@
| find_repeated (tab, past, t::terms) =
case try Data.dest_coeff t of
SOME(n,u) =>
- (case Termtab.lookup (tab, u) of
+ (case Termtab.curried_lookup tab u of
SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
- | NONE => find_repeated (Termtab.update ((u,n), tab),
+ | NONE => find_repeated (Termtab.curried_update (u, n) tab,
t::past, terms))
| NONE => find_repeated (tab, t::past, terms);