diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/nat_simprocs.ML
--- a/src/HOL/Tools/nat_simprocs.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
-(*  Title:      HOL/nat_simprocs.ML
-    ID:         $Id$
+(*  Title:      HOL/Tools/nat_simprocs.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
 
 Simprocs for nat numerals.
 *)
@@ -81,7 +79,7 @@
 
 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
 fun dest_coeff t =
-    let val ts = sort Term.term_ord (dest_prod t)
+    let val ts = sort TermOrd.term_ord (dest_prod t)
         val (n, _, ts') = find_first_numeral [] ts
                           handle TERM _ => (1, one, ts)
     in (n, mk_prod ts') end;