src/HOL/Tools/int_arith.ML
changeset 29269 5c25a2012975
parent 28952 15a4b2cf8c34
child 30496 7cdcc9dd95cb
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      HOL/int_arith1.ML
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Tools/int_arith1.ML
     1.7      Authors:    Larry Paulson and Tobias Nipkow
     1.8  
     1.9  Simprocs and decision procedure for linear arithmetic.
    1.10 @@ -66,12 +65,12 @@
    1.11      EQUAL => int_ord (Int.sign i, Int.sign j) 
    1.12    | ord => ord);
    1.13  
    1.14 -(*This resembles Term.term_ord, but it puts binary numerals before other
    1.15 +(*This resembles TermOrd.term_ord, but it puts binary numerals before other
    1.16    non-atomic terms.*)
    1.17  local open Term 
    1.18  in 
    1.19  fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    1.20 -      (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    1.21 +      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
    1.22    | numterm_ord
    1.23       (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    1.24       num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    1.25 @@ -81,7 +80,7 @@
    1.26        (case int_ord (size_of_term t, size_of_term u) of
    1.27          EQUAL =>
    1.28            let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    1.29 -            (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    1.30 +            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    1.31            end
    1.32        | ord => ord)
    1.33  and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    1.34 @@ -164,7 +163,7 @@
    1.35  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    1.36  fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
    1.37    | dest_coeff sign t =
    1.38 -    let val ts = sort Term.term_ord (dest_prod t)
    1.39 +    let val ts = sort TermOrd.term_ord (dest_prod t)
    1.40          val (n, ts') = find_first_numeral [] ts
    1.41                            handle TERM _ => (1, ts)
    1.42      in (sign*n, mk_prod (Term.fastype_of t) ts') end;