--- 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;