# HG changeset patch
# User paulson
# Date 966594641 -7200
# Node ID aa3b82085e072b5f4f565e993d1b2c37afbad817
# Parent  20ae97cd2a1608d43941065ed6fea5200a1182e7
now allows dest_coeff to fail

diff -r 20ae97cd2a16 -r aa3b82085e07 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Fri Aug 18 11:14:23 2000 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Fri Aug 18 12:30:41 2000 +0200
@@ -46,22 +46,22 @@
 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
       raise TERM("combine_numerals: remove", [])  
   | remove (m, u, t::terms) =
-      let val (n,v) = Data.dest_coeff t 
-      in  if m=n andalso u aconv v then terms
-          else t :: remove (m, u, terms)
-      end;
+      case try Data.dest_coeff t of
+	  Some(n,v) => if m=n andalso u aconv v then terms
+		       else t :: remove (m, u, terms)
+	| None      =>  t :: remove (m, u, terms);
 
 (*a left-to-right scan of terms, seeking another term of the form #n*u, where
   #m*u is already in terms for some m*)
 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
   | find_repeated (tab, past, t::terms) =
-      let val (n,u) = Data.dest_coeff t 
-      in  
-	  case Termtab.lookup (tab, u) of
-	      Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
-	    | None => find_repeated (Termtab.update ((u,n), tab), 
-				     t::past,  terms)
-      end;
+      case try Data.dest_coeff t of
+	  Some(n,u) => 
+	      (case Termtab.lookup (tab, u) of
+		  Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
+		| None => find_repeated (Termtab.update ((u,n), tab), 
+					 t::past,  terms))
+	| None => find_repeated (tab, t::past, terms);
 
 (*the simplification procedure*)
 fun proc sg _ t =