diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Wed Dec 31 00:08:14 2008 +0100 +++ b/src/HOL/Tools/int_arith.ML Wed Dec 31 15:30:10 2008 +0100 @@ -1,5 +1,4 @@ -(* Title: HOL/int_arith1.ML - ID: \$Id\$ +(* Title: HOL/Tools/int_arith1.ML Authors: Larry Paulson and Tobias Nipkow Simprocs and decision procedure for linear arithmetic. @@ -66,12 +65,12 @@ EQUAL => int_ord (Int.sign i, Int.sign j) | ord => ord); -(*This resembles Term.term_ord, but it puts binary numerals before other +(*This resembles TermOrd.term_ord, but it puts binary numerals before other non-atomic terms.*) local open Term in fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = - (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) + (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) | numterm_ord (Const(@{const_name Int.number_of}, _) \$ v, Const(@{const_name Int.number_of}, _) \$ w) = num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) @@ -81,7 +80,7 @@ (case int_ord (size_of_term t, size_of_term u) of EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) + (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) end | ord => ord) and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) @@ -164,7 +163,7 @@ (*Express t as a product of (possibly) a numeral with other sorted terms*) fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) \$ t) = dest_coeff (~sign) t | dest_coeff sign 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, ts) in (sign*n, mk_prod (Term.fastype_of t) ts') end;