# 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 =