--- a/src/Provers/Arith/cancel_factor.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/Arith/cancel_factor.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Provers/Arith/cancel_factor.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
@@ -36,7 +35,7 @@
if t aconv u then (u, k + 1) :: uks
else (t, 1) :: (u, k) :: uks;
-fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);
+fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
(* divide sum *)