src/ZF/int_arith.ML
changeset 29269 5c25a2012975
parent 27237 c94eefffc3a5
child 30607 c3d1590debd8
     1.1 --- a/src/ZF/int_arith.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/ZF/int_arith.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:      ZF/int_arith.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Larry Paulson
     1.7 -    Copyright   2000  University of Cambridge
     1.8  
     1.9  Simprocs for linear arithmetic.
    1.10  *)
    1.11 @@ -72,7 +70,7 @@
    1.12  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    1.13  fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
    1.14    | dest_coeff sign t =
    1.15 -    let val ts = sort Term.term_ord (dest_prod t)
    1.16 +    let val ts = sort TermOrd.term_ord (dest_prod t)
    1.17          val (n, ts') = find_first_numeral [] ts
    1.18                            handle TERM _ => (1, ts)
    1.19      in (sign*n, mk_prod ts') end;