--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sat Feb 27 22:52:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sat Feb 27 23:13:01 2010 +0100
@@ -436,14 +436,14 @@
val empty = [];
val extend = I;
fun merge (ts1, ts2) =
- OrdList.union TermOrd.fast_term_ord ts1 ts2;
+ OrdList.union Term_Ord.fast_term_ord ts1 ts2;
)
val get = Terms.get;
fun add raw_t thy =
let val t = Sign.cert_term thy raw_t
- in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end;
+ in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
end;
*}
--- a/src/HOL/Algebra/abstract/Ring2.thy Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Feb 27 23:13:01 2010 +0100
@@ -207,7 +207,7 @@
@{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
| ring_ord _ = ~1;
-fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
+fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
val ring_ss = HOL_basic_ss settermless termless_ring addsimps
[thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
--- a/src/HOL/Algebra/ringsimp.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sat Feb 27 23:13:01 2010 +0100
@@ -46,7 +46,7 @@
val ops = map (fst o Term.strip_comb) ts;
fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
| ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
- fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
+ fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
fun algebra_tac ctxt =
--- a/src/HOL/Groups.thy Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Groups.thy Sat Feb 27 23:13:01 2010 +0100
@@ -1216,7 +1216,7 @@
@{const_name Groups.uminus}, @{const_name Groups.minus}]
| agrp_ord _ = ~1;
-fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
+fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
local
val ac1 = mk_meta_eq @{thm add_assoc};
--- a/src/HOL/Import/shuffler.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Import/shuffler.ML Sat Feb 27 23:13:01 2010 +0100
@@ -351,7 +351,7 @@
fun equals_fun thy assume t =
case t of
- Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+ Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
| _ => NONE
fun eta_expand thy assumes origt =
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Feb 27 23:13:01 2010 +0100
@@ -1189,7 +1189,7 @@
local
open Conv
val concl = Thm.dest_arg o cprop_of
- fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
+ fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS
in
(* FIXME: Replace tryfind by get_first !! *)
fun real_nonlinear_prover proof_method ctxt =
@@ -1279,7 +1279,7 @@
local
open Conv
- fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
+ fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS
val concl = Thm.dest_arg o cprop_of
val shuffle1 =
fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) })
--- a/src/HOL/Library/normarith.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Library/normarith.ML Sat Feb 27 23:13:01 2010 +0100
@@ -216,7 +216,7 @@
let
val l = headvector lt
val r = headvector rt
- in (case TermOrd.fast_term_ord (l,r) of
+ in (case Term_Ord.fast_term_ord (l,r) of
LESS => (apply_pthb then_conv arg_conv vector_add_conv
then_conv apply_pthd) ct
| GREATER => (apply_pthc then_conv arg_conv vector_add_conv
@@ -378,7 +378,7 @@
local
val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
- fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
+ fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
(* FIXME: Lookup in the context every time!!! Fix this !!!*)
fun splitequation ctxt th acc =
let
--- a/src/HOL/Library/positivstellensatz.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Sat Feb 27 23:13:01 2010 +0100
@@ -61,9 +61,9 @@
structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
-structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
+structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
-val cterm_ord = TermOrd.fast_term_ord o pairself term_of
+val cterm_ord = Term_Ord.fast_term_ord o pairself term_of
structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
@@ -745,7 +745,7 @@
fun gen_prover_real_arith ctxt prover =
let
- fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
+ fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
val {add,mul,neg,pow,sub,main} =
Normalizer.semiring_normalizers_ord_wrapper ctxt
(the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
--- a/src/HOL/Mutabelle/mutabelle.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Sat Feb 27 23:13:01 2010 +0100
@@ -361,7 +361,7 @@
val t' = canonize_term t comms;
val u' = canonize_term u comms;
in
- if s mem comms andalso TermOrd.termless (u', t')
+ if s mem comms andalso Term_Ord.termless (u', t')
then Const (s, T) $ u' $ t'
else Const (s, T) $ t' $ u'
end
--- a/src/HOL/SMT/Tools/smt_translate.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML Sat Feb 27 23:13:01 2010 +0100
@@ -253,9 +253,9 @@
| atoms_ord (SNum (i, _), SNum (j, _)) = int_ord (i, j)
| atoms_ord _ = sys_error "atoms_ord"
- fun types_ord (SConst (_, T), SConst (_, U)) = TermOrd.typ_ord (T, U)
- | types_ord (SFree (_, T), SFree (_, U)) = TermOrd.typ_ord (T, U)
- | types_ord (SNum (_, T), SNum (_, U)) = TermOrd.typ_ord (T, U)
+ fun types_ord (SConst (_, T), SConst (_, U)) = Term_Ord.typ_ord (T, U)
+ | types_ord (SFree (_, T), SFree (_, U)) = Term_Ord.typ_ord (T, U)
+ | types_ord (SNum (_, T), SNum (_, U)) = Term_Ord.typ_ord (T, U)
| types_ord _ = sys_error "types_ord"
fun fast_sym_ord tu =
--- a/src/HOL/Statespace/DistinctTreeProver.thy Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Sat Feb 27 23:13:01 2010 +0100
@@ -645,9 +645,9 @@
val const_decls = map (fn i => Syntax.no_syn
("const" ^ string_of_int i,Type ("nat",[]))) nums
-val consts = sort TermOrd.fast_term_ord
+val consts = sort Term_Ord.fast_term_ord
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort TermOrd.fast_term_ord
+val consts' = sort Term_Ord.fast_term_ord
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
--- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Feb 27 23:13:01 2010 +0100
@@ -79,7 +79,7 @@
| bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
fun find_tree e t =
- (case bin_find_tree TermOrd.fast_term_ord e t of
+ (case bin_find_tree Term_Ord.fast_term_ord e t of
NONE => lin_find_tree e t
| x => x);
--- a/src/HOL/Tools/Function/termination.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Sat Feb 27 23:13:01 2010 +0100
@@ -51,9 +51,10 @@
open Function_Lib
-val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
+val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord
structure Term2tab = Table(type key = term * term val ord = term2_ord);
-structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
+structure Term3tab =
+ Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord);
(** Analyzing binary trees **)
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sat Feb 27 23:13:01 2010 +0100
@@ -689,7 +689,7 @@
val cjs = conjs tm
val rawvars = fold_rev (fn eq => fn a =>
grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs []
- val vars = sort (fn (x, y) => TermOrd.term_ord(term_of x,term_of y))
+ val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y))
(distinct (op aconvc) rawvars)
in (vars,map (grobify_equation vars) cjs)
end;
@@ -898,7 +898,7 @@
val vars = filter (fn v => free_in v eq) evs
val (qs,p) = isolate_monomials vars eq
val rs = ideal (qs @ ps) p
- (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
+ (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t))
in (eq, take (length qs) rs ~~ vars)
end;
fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sat Feb 27 23:13:01 2010 +0100
@@ -636,7 +636,7 @@
val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
-fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
+fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
{conv, dest_const, mk_const, is_const}) ord =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 27 23:13:01 2010 +0100
@@ -359,7 +359,7 @@
not standard orelse T = nat_T orelse is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
- |> sort TermOrd.typ_ord
+ |> sort Term_Ord.typ_ord
val _ = if verbose andalso binary_ints = SOME true andalso
exists (member (op =) [nat_T, int_T]) all_Ts then
print_v (K "The option \"binary_ints\" will be ignored because \
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Feb 27 23:13:01 2010 +0100
@@ -1122,7 +1122,7 @@
(* term list -> (indexname * typ) list *)
fun special_bounds ts =
- fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
+ fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
(* indexname * typ -> term -> term *)
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Feb 27 23:13:01 2010 +0100
@@ -103,7 +103,7 @@
(case nice_term_ord (t11, t21) of
EQUAL => nice_term_ord (t12, t22)
| ord => ord)
- | _ => TermOrd.fast_term_ord tp
+ | _ => Term_Ord.fast_term_ord tp
(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
fun tuple_list_for_name rel_table bounds name =
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Feb 27 23:13:01 2010 +0100
@@ -400,13 +400,13 @@
| name_ord (_, BoundName _) = GREATER
| name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) =
(case fast_string_ord (s1, s2) of
- EQUAL => TermOrd.typ_ord (T1, T2)
+ EQUAL => Term_Ord.typ_ord (T1, T2)
| ord => ord)
| name_ord (FreeName _, _) = LESS
| name_ord (_, FreeName _) = GREATER
| name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) =
(case fast_string_ord (s1, s2) of
- EQUAL => TermOrd.typ_ord (T1, T2)
+ EQUAL => Term_Ord.typ_ord (T1, T2)
| ord => ord)
| name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Feb 27 23:13:01 2010 +0100
@@ -247,7 +247,7 @@
let
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
- val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
+ val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last
in
list_comb (Const (s0, T --> T --> body_type T0),
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
@@ -815,7 +815,7 @@
| call_sets [] uss vs = vs :: call_sets uss [] []
| call_sets ([] :: _) _ _ = []
| call_sets ((t :: ts) :: tss) uss vs =
- OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
+ OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
val sets = call_sets (fun_calls t [] []) [] []
val indexed_sets = sets ~~ (index_seq 0 (length sets))
in
@@ -830,7 +830,7 @@
(* hol_context -> styp -> term list -> (int * term option) list *)
fun static_args_in_terms hol_ctxt x =
map (static_args_in_term hol_ctxt x)
- #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
+ #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
(* (int * term option) list -> (int * term) list -> int list *)
fun overlapping_indices [] _ = []
@@ -882,7 +882,7 @@
val _ = not (null fixed_js) orelse raise SAME ()
val fixed_args = filter_indices fixed_js args
val vars = fold Term.add_vars fixed_args []
- |> sort (TermOrd.fast_indexname_ord o pairself fst)
+ |> sort (Term_Ord.fast_indexname_ord o pairself fst)
val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
fixed_args []
|> sort int_ord
@@ -972,7 +972,7 @@
fun generality (js, _, _) = ~(length js)
(* special_triple -> special_triple -> bool *)
fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
- x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
+ x1 <> x2 andalso OrdList.subset (prod_ord int_ord Term_Ord.term_ord)
(j2 ~~ t2, j1 ~~ t1)
(* typ -> special_triple list -> special_triple list -> special_triple list
-> term list -> term list *)
--- a/src/HOL/Tools/Qelim/langford.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML Sat Feb 27 23:13:01 2010 +0100
@@ -210,7 +210,7 @@
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
- val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
+ val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
--- a/src/HOL/Tools/Qelim/presburger.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Sat Feb 27 23:13:01 2010 +0100
@@ -103,7 +103,7 @@
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
- val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
+ val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Feb 27 23:13:01 2010 +0100
@@ -80,7 +80,7 @@
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
fun dest_coeff 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, one, ts)
in (n, mk_prod ts') end;
--- 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)
--- a/src/HOL/Tools/record.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/record.ML Sat Feb 27 23:13:01 2010 +0100
@@ -1100,7 +1100,7 @@
fun get_accupd_simps thy term defset =
let
val (acc, [body]) = strip_comb term;
- val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
+ val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
fun get_simp upd =
let
(* FIXME fresh "f" (!?) *)
--- a/src/HOL/Tools/sat_funcs.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Sat Feb 27 23:13:01 2010 +0100
@@ -320,7 +320,7 @@
(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
(* terms sorted in descending order, while only linear for terms *)
(* sorted in ascending order *)
- val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
+ val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
val _ = if !trace_sat then
tracing ("Sorted non-trivial clauses:\n" ^
cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
--- a/src/Provers/Arith/cancel_factor.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Provers/Arith/cancel_factor.ML Sat Feb 27 23:13:01 2010 +0100
@@ -35,7 +35,7 @@
if t aconv u then (u, k + 1) :: uks
else (t, 1) :: (u, k) :: uks;
-fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
+fun count_terms ts = foldr ins_term (sort Term_Ord.term_ord ts, []);
(* divide sum *)
--- a/src/Provers/Arith/cancel_sums.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Provers/Arith/cancel_sums.ML Sat Feb 27 23:13:01 2010 +0100
@@ -37,11 +37,11 @@
fun cons2 y (x, ys, z) = (x, y :: ys, z);
fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
-(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*)
+(*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*)
fun cancel ts [] vs = (ts, [], vs)
| cancel [] us vs = ([], us, vs)
| cancel (t :: ts) (u :: us) vs =
- (case TermOrd.term_ord (t, u) of
+ (case Term_Ord.term_ord (t, u) of
EQUAL => cancel ts us (t :: vs)
| LESS => cons1 t (cancel ts (u :: us) vs)
| GREATER => cons2 u (cancel (t :: ts) us vs));
@@ -63,7 +63,7 @@
| SOME bal =>
let
val thy = ProofContext.theory_of (Simplifier.the_context ss);
- val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal;
+ val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal;
val (ts', us', vs) = cancel ts us [];
in
if null vs then NONE
--- a/src/Pure/Isar/rule_cases.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/Isar/rule_cases.ML Sat Feb 27 23:13:01 2010 +0100
@@ -379,7 +379,7 @@
local
fun equal_cterms ts us =
- is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
+ is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
fun prep_rule n th =
let
--- a/src/Pure/Tools/find_theorems.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sat Feb 27 23:13:01 2010 +0100
@@ -364,7 +364,7 @@
fun rem_thm_dups nicer xs =
xs ~~ (1 upto length xs)
- |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
+ |> sort (Term_Ord.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
|> rem_cdups nicer
|> sort (int_ord o pairself #2)
|> map #1;
--- a/src/Pure/envir.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/envir.ML Sat Feb 27 23:13:01 2010 +0100
@@ -139,7 +139,7 @@
(case t of
Var (nT as (name', T)) =>
if a = name' then env (*cycle!*)
- else if TermOrd.indexname_ord (a, name') = LESS then
+ else if Term_Ord.indexname_ord (a, name') = LESS then
(case lookup (env, nT) of (*if already assigned, chase*)
NONE => update ((nT, Var (a, T)), env)
| SOME u => vupdate ((aU, u), env))
--- a/src/Pure/facts.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/facts.ML Sat Feb 27 23:13:01 2010 +0100
@@ -171,7 +171,7 @@
(* indexed props *)
-val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of;
+val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of;
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
fun could_unify (Facts {props, ...}) = Net.unify_term props;
--- a/src/Pure/meta_simplifier.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/meta_simplifier.ML Sat Feb 27 23:13:01 2010 +0100
@@ -755,7 +755,7 @@
mk_eq_True = K NONE,
reorient = default_reorient};
-val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
+val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
(* merge *) (*NOTE: ignores some fields of 2nd simpset*)
--- a/src/Pure/more_thm.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/more_thm.ML Sat Feb 27 23:13:01 2010 +0100
@@ -151,12 +151,12 @@
val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
in
- (case TermOrd.fast_term_ord (prop1, prop2) of
+ (case Term_Ord.fast_term_ord (prop1, prop2) of
EQUAL =>
- (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of
+ (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of
EQUAL =>
- (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of
- EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2)
+ (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of
+ EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2)
| ord => ord)
| ord => ord)
| ord => ord)
@@ -165,7 +165,7 @@
(* tables and caches *)
-structure Ctermtab = Table(type key = cterm val ord = TermOrd.fast_term_ord o pairself Thm.term_of);
+structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o pairself Thm.term_of);
structure Thmtab = Table(type key = thm val ord = thm_ord);
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
--- a/src/Pure/old_term.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/old_term.ML Sat Feb 27 23:13:01 2010 +0100
@@ -75,7 +75,7 @@
(*Accumulates the Vars in the term, suppressing duplicates.*)
fun add_term_vars (t, vars: term list) = case t of
- Var _ => OrdList.insert TermOrd.term_ord t vars
+ Var _ => OrdList.insert Term_Ord.term_ord t vars
| Abs (_,_,body) => add_term_vars(body,vars)
| f$t => add_term_vars (f, add_term_vars(t, vars))
| _ => vars;
@@ -84,7 +84,7 @@
(*Accumulates the Frees in the term, suppressing duplicates.*)
fun add_term_frees (t, frees: term list) = case t of
- Free _ => OrdList.insert TermOrd.term_ord t frees
+ Free _ => OrdList.insert Term_Ord.term_ord t frees
| Abs (_,_,body) => add_term_frees(body,frees)
| f$t => add_term_frees (f, add_term_frees(t, frees))
| _ => frees;
--- a/src/Pure/pattern.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/pattern.ML Sat Feb 27 23:13:01 2010 +0100
@@ -226,7 +226,7 @@
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
end;
- in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
+ in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
if T = U then env
--- a/src/Pure/proofterm.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/proofterm.ML Sat Feb 27 23:13:01 2010 +0100
@@ -214,7 +214,7 @@
(* proof body *)
-val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
+val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
val merge_oracles = OrdList.union oracle_ord;
--- a/src/Pure/search.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/search.ML Sat Feb 27 23:13:01 2010 +0100
@@ -197,7 +197,7 @@
structure Thm_Heap = Heap
(
type elem = int * thm;
- val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of);
+ val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of);
);
val trace_BEST_FIRST = Unsynchronized.ref false;
--- a/src/Pure/sorts.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/sorts.ML Sat Feb 27 23:13:01 2010 +0100
@@ -71,13 +71,13 @@
(** ordered lists of sorts **)
-val make = OrdList.make TermOrd.sort_ord;
-val subset = OrdList.subset TermOrd.sort_ord;
-val union = OrdList.union TermOrd.sort_ord;
-val subtract = OrdList.subtract TermOrd.sort_ord;
+val make = OrdList.make Term_Ord.sort_ord;
+val subset = OrdList.subset Term_Ord.sort_ord;
+val union = OrdList.union Term_Ord.sort_ord;
+val subtract = OrdList.subtract Term_Ord.sort_ord;
-val remove_sort = OrdList.remove TermOrd.sort_ord;
-val insert_sort = OrdList.insert TermOrd.sort_ord;
+val remove_sort = OrdList.remove Term_Ord.sort_ord;
+val insert_sort = OrdList.insert Term_Ord.sort_ord;
fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
| insert_typ (TVar (_, S)) Ss = insert_sort S Ss
--- a/src/Pure/term_ord.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/term_ord.ML Sat Feb 27 23:13:01 2010 +0100
@@ -29,7 +29,7 @@
val term_cache: (term -> 'a) -> term -> 'a
end;
-structure TermOrd: TERM_ORD =
+structure Term_Ord: TERM_ORD =
struct
(* fast syntactic ordering -- tuned for inequalities *)
@@ -223,11 +223,11 @@
end;
-structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
+structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
open Basic_Term_Ord;
-structure Var_Graph = Graph(type key = indexname val ord = TermOrd.fast_indexname_ord);
-structure Sort_Graph = Graph(type key = sort val ord = TermOrd.sort_ord);
-structure Typ_Graph = Graph(type key = typ val ord = TermOrd.typ_ord);
-structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
+structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
+structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
+structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
+structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
--- a/src/Pure/term_subst.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/term_subst.ML Sat Feb 27 23:13:01 2010 +0100
@@ -198,9 +198,9 @@
fun zero_var_indexes_inst ts =
let
- val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []);
+ val tvars = sort Term_Ord.tvar_ord (fold Term.add_tvars ts []);
val instT = map (apsnd TVar) (zero_var_inst tvars);
- val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
+ val vars = sort Term_Ord.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
val inst = map (apsnd Var) (zero_var_inst vars);
in (instT, inst) end;
--- a/src/Pure/thm.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/thm.ML Sat Feb 27 23:13:01 2010 +0100
@@ -384,9 +384,9 @@
fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
-val union_hyps = OrdList.union TermOrd.fast_term_ord;
-val insert_hyps = OrdList.insert TermOrd.fast_term_ord;
-val remove_hyps = OrdList.remove TermOrd.fast_term_ord;
+val union_hyps = OrdList.union Term_Ord.fast_term_ord;
+val insert_hyps = OrdList.insert Term_Ord.fast_term_ord;
+val remove_hyps = OrdList.remove Term_Ord.fast_term_ord;
(* merge theories of cterms/thms -- trivial absorption only *)
--- a/src/Pure/unify.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/unify.ML Sat Feb 27 23:13:01 2010 +0100
@@ -558,7 +558,7 @@
if Term.eq_ix (v, w) then (*...occur check would falsely return true!*)
if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
else raise TERM ("add_ffpair: Var name confusion", [t,u])
- else if TermOrd.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
+ else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
clean_ffpair thy ((rbinder, u, t), (env,tpairs))
else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
| _ => raise TERM ("add_ffpair: Vars expected", [t,u])
--- a/src/Tools/Compute_Oracle/linker.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML Sat Feb 27 23:13:01 2010 +0100
@@ -50,7 +50,7 @@
| constant_of _ = raise Link "constant_of"
fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
-fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) TermOrd.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
+fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term_Ord.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
@@ -70,7 +70,7 @@
handle Type.TYPE_MATCH => NONE
fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
- (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
+ (list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))) (Vartab.dest A, Vartab.dest B)
structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
@@ -380,7 +380,7 @@
ComputeThm (hyps, shyps, prop)
end
-val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord
+val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
--- a/src/ZF/arith_data.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/ZF/arith_data.ML Sat Feb 27 23:13:01 2010 +0100
@@ -104,7 +104,7 @@
(*Dummy version: the "coefficient" is always 1.
In the result, the factors are sorted terms*)
-fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
+fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t)));
(*Find first coefficient-term THAT MATCHES u*)
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
--- a/src/ZF/int_arith.ML Sat Feb 27 22:52:25 2010 +0100
+++ b/src/ZF/int_arith.ML Sat Feb 27 23:13:01 2010 +0100
@@ -95,7 +95,7 @@
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ 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 ts') end;