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