--- a/src/Provers/Arith/extract_common_term.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Provers/Arith/extract_common_term.ML Thu Mar 03 12:43:01 2005 +0100
@@ -42,10 +42,10 @@
(*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
fun find_common (terms1,terms2) =
- let val tab2 = foldl update_by_coeff (Termtab.empty, terms2)
+ let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
fun seek [] = raise TERM("find_common", [])
| seek (u::terms) =
- if is_some (Termtab.lookup (tab2, u)) then u
+ if isSome (Termtab.lookup (tab2, u)) then u
else seek terms
in seek terms1 end;
@@ -68,7 +68,7 @@
Data.mk_bal (Data.mk_sum T (u::terms1'),
Data.mk_sum T (u::terms2')))
in
- apsome Data.simplify_meta_eq reshape
+ Option.map Data.simplify_meta_eq reshape
end
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)