diff -r 980d4194a212 -r b48ab741683b src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/ZF/arith_data.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -104,7 +104,7 @@
 
 (*Dummy version: the "coefficient" is always 1.
   In the result, the factors are sorted terms*)
-fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
+fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t)));
 
 (*Find first coefficient-term THAT MATCHES u*)
 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])