--- a/src/HOL/Tools/numeral_simprocs.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Feb 27 23:13:01 2010 +0100
@@ -74,7 +74,7 @@
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
- let val ts = sort TermOrd.term_ord (dest_prod t)
+ let val ts = sort Term_Ord.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;
@@ -124,12 +124,12 @@
EQUAL => int_ord (Int.sign i, Int.sign j)
| ord => ord);
-(*This resembles TermOrd.term_ord, but it puts binary numerals before other
+(*This resembles Term_Ord.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 => TermOrd.typ_ord (T, U) | ord => ord)
+ (case numterm_ord (t, u) of EQUAL => Term_Ord.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)
@@ -139,7 +139,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 TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
+ (case Term_Ord.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)