src/HOL/Tools/nat_numeral_simprocs.ML

--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -80,7 +80,7 @@
 
 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
 fun dest_coeff 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, one, ts)
     in (n, mk_prod ts') end;