--- a/src/ZF/int_arith.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/ZF/int_arith.ML Sat Feb 27 23:13:01 2010 +0100
@@ -95,7 +95,7 @@
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
- let val ts = sort TermOrd.term_ord (dest_prod t)
+ let val ts = sort Term_Ord.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*n, mk_prod ts') end;