modernized structure Term_Ord;
authorwenzelm
Sat Feb 27 23:13:01 2010 +0100 (2010-02-27 ago)
changeset 35408b48ab741683b
parent 35407 980d4194a212
child 35409 5c5bb83f2bae
modernized structure Term_Ord;
doc-src/IsarImplementation/Thy/Prelim.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Groups.thy
src/HOL/Import/shuffler.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Mutabelle/mutabelle.ML
src/HOL/SMT/Tools/smt_translate.ML
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Tools/sat_funcs.ML
src/Provers/Arith/cancel_factor.ML
src/Provers/Arith/cancel_sums.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Tools/find_theorems.ML
src/Pure/envir.ML
src/Pure/facts.ML
src/Pure/meta_simplifier.ML
src/Pure/more_thm.ML
src/Pure/old_term.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/search.ML
src/Pure/sorts.ML
src/Pure/term_ord.ML
src/Pure/term_subst.ML
src/Pure/thm.ML
src/Pure/unify.ML
src/Tools/Compute_Oracle/linker.ML
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Feb 27 22:52:25 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Feb 27 23:13:01 2010 +0100
     1.3 @@ -436,14 +436,14 @@
     1.4      val empty = [];
     1.5      val extend = I;
     1.6      fun merge (ts1, ts2) =
     1.7 -      OrdList.union TermOrd.fast_term_ord ts1 ts2;
     1.8 +      OrdList.union Term_Ord.fast_term_ord ts1 ts2;
     1.9    )
    1.10  
    1.11    val get = Terms.get;
    1.12  
    1.13    fun add raw_t thy =
    1.14      let val t = Sign.cert_term thy raw_t
    1.15 -    in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end;
    1.16 +    in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
    1.17  
    1.18    end;
    1.19  *}
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Feb 27 22:52:25 2010 +0100
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Feb 27 23:13:01 2010 +0100
     2.3 @@ -207,7 +207,7 @@
     2.4          @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
     2.5    | ring_ord _ = ~1;
     2.6  
     2.7 -fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
     2.8 +fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
     2.9  
    2.10  val ring_ss = HOL_basic_ss settermless termless_ring addsimps
    2.11    [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
     3.1 --- a/src/HOL/Algebra/ringsimp.ML	Sat Feb 27 22:52:25 2010 +0100
     3.2 +++ b/src/HOL/Algebra/ringsimp.ML	Sat Feb 27 23:13:01 2010 +0100
     3.3 @@ -46,7 +46,7 @@
     3.4      val ops = map (fst o Term.strip_comb) ts;
     3.5      fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
     3.6        | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
     3.7 -    fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
     3.8 +    fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
     3.9    in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
    3.10  
    3.11  fun algebra_tac ctxt =
     4.1 --- a/src/HOL/Groups.thy	Sat Feb 27 22:52:25 2010 +0100
     4.2 +++ b/src/HOL/Groups.thy	Sat Feb 27 23:13:01 2010 +0100
     4.3 @@ -1216,7 +1216,7 @@
     4.4          @{const_name Groups.uminus}, @{const_name Groups.minus}]
     4.5    | agrp_ord _ = ~1;
     4.6  
     4.7 -fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
     4.8 +fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
     4.9  
    4.10  local
    4.11    val ac1 = mk_meta_eq @{thm add_assoc};
     5.1 --- a/src/HOL/Import/shuffler.ML	Sat Feb 27 22:52:25 2010 +0100
     5.2 +++ b/src/HOL/Import/shuffler.ML	Sat Feb 27 23:13:01 2010 +0100
     5.3 @@ -351,7 +351,7 @@
     5.4  
     5.5  fun equals_fun thy assume t =
     5.6      case t of
     5.7 -        Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
     5.8 +        Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
     5.9        | _ => NONE
    5.10  
    5.11  fun eta_expand thy assumes origt =
     6.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat Feb 27 22:52:25 2010 +0100
     6.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat Feb 27 23:13:01 2010 +0100
     6.3 @@ -1189,7 +1189,7 @@
     6.4  local
     6.5    open Conv
     6.6    val concl = Thm.dest_arg o cprop_of
     6.7 -  fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
     6.8 +  fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS
     6.9  in
    6.10    (* FIXME: Replace tryfind by get_first !! *)
    6.11  fun real_nonlinear_prover proof_method ctxt =
    6.12 @@ -1279,7 +1279,7 @@
    6.13  
    6.14  local
    6.15   open Conv
    6.16 -  fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
    6.17 +  fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS
    6.18   val concl = Thm.dest_arg o cprop_of
    6.19   val shuffle1 =
    6.20     fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) })
     7.1 --- a/src/HOL/Library/normarith.ML	Sat Feb 27 22:52:25 2010 +0100
     7.2 +++ b/src/HOL/Library/normarith.ML	Sat Feb 27 23:13:01 2010 +0100
     7.3 @@ -216,7 +216,7 @@
     7.4        let 
     7.5         val l = headvector lt 
     7.6         val r = headvector rt
     7.7 -      in (case TermOrd.fast_term_ord (l,r) of
     7.8 +      in (case Term_Ord.fast_term_ord (l,r) of
     7.9           LESS => (apply_pthb then_conv arg_conv vector_add_conv 
    7.10                    then_conv apply_pthd) ct
    7.11          | GREATER => (apply_pthc then_conv arg_conv vector_add_conv 
    7.12 @@ -378,7 +378,7 @@
    7.13  local
    7.14   val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
    7.15   fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
    7.16 - fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
    7.17 + fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
    7.18    (* FIXME: Lookup in the context every time!!! Fix this !!!*)
    7.19   fun splitequation ctxt th acc =
    7.20    let 
     8.1 --- a/src/HOL/Library/positivstellensatz.ML	Sat Feb 27 22:52:25 2010 +0100
     8.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sat Feb 27 23:13:01 2010 +0100
     8.3 @@ -61,9 +61,9 @@
     8.4  structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
     8.5  structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
     8.6  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
     8.7 -structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
     8.8 +structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
     8.9  
    8.10 -val cterm_ord = TermOrd.fast_term_ord o pairself term_of
    8.11 +val cterm_ord = Term_Ord.fast_term_ord o pairself term_of
    8.12  
    8.13  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
    8.14  
    8.15 @@ -745,7 +745,7 @@
    8.16  
    8.17  fun gen_prover_real_arith ctxt prover = 
    8.18   let
    8.19 -  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
    8.20 +  fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
    8.21    val {add,mul,neg,pow,sub,main} = 
    8.22       Normalizer.semiring_normalizers_ord_wrapper ctxt
    8.23        (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
     9.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sat Feb 27 22:52:25 2010 +0100
     9.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Sat Feb 27 23:13:01 2010 +0100
     9.3 @@ -361,7 +361,7 @@
     9.4     val t' = canonize_term t comms;
     9.5     val u' = canonize_term u comms;
     9.6   in 
     9.7 -   if s mem comms andalso TermOrd.termless (u', t')
     9.8 +   if s mem comms andalso Term_Ord.termless (u', t')
     9.9     then Const (s, T) $ u' $ t'
    9.10     else Const (s, T) $ t' $ u'
    9.11   end
    10.1 --- a/src/HOL/SMT/Tools/smt_translate.ML	Sat Feb 27 22:52:25 2010 +0100
    10.2 +++ b/src/HOL/SMT/Tools/smt_translate.ML	Sat Feb 27 23:13:01 2010 +0100
    10.3 @@ -253,9 +253,9 @@
    10.4        | atoms_ord (SNum (i, _), SNum (j, _)) = int_ord (i, j)
    10.5        | atoms_ord _ = sys_error "atoms_ord"
    10.6  
    10.7 -    fun types_ord (SConst (_, T), SConst (_, U)) = TermOrd.typ_ord (T, U)
    10.8 -      | types_ord (SFree (_, T), SFree (_, U)) = TermOrd.typ_ord (T, U)
    10.9 -      | types_ord (SNum (_, T), SNum (_, U)) = TermOrd.typ_ord (T, U)
   10.10 +    fun types_ord (SConst (_, T), SConst (_, U)) = Term_Ord.typ_ord (T, U)
   10.11 +      | types_ord (SFree (_, T), SFree (_, U)) = Term_Ord.typ_ord (T, U)
   10.12 +      | types_ord (SNum (_, T), SNum (_, U)) = Term_Ord.typ_ord (T, U)
   10.13        | types_ord _ = sys_error "types_ord"
   10.14  
   10.15      fun fast_sym_ord tu =
    11.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Sat Feb 27 22:52:25 2010 +0100
    11.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sat Feb 27 23:13:01 2010 +0100
    11.3 @@ -645,9 +645,9 @@
    11.4  val const_decls = map (fn i => Syntax.no_syn 
    11.5                                   ("const" ^ string_of_int i,Type ("nat",[]))) nums
    11.6  
    11.7 -val consts = sort TermOrd.fast_term_ord 
    11.8 +val consts = sort Term_Ord.fast_term_ord 
    11.9                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
   11.10 -val consts' = sort TermOrd.fast_term_ord 
   11.11 +val consts' = sort Term_Ord.fast_term_ord 
   11.12                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
   11.13  
   11.14  val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
    12.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sat Feb 27 22:52:25 2010 +0100
    12.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sat Feb 27 23:13:01 2010 +0100
    12.3 @@ -79,7 +79,7 @@
    12.4    | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
    12.5  
    12.6  fun find_tree e t =
    12.7 -  (case bin_find_tree TermOrd.fast_term_ord e t of
    12.8 +  (case bin_find_tree Term_Ord.fast_term_ord e t of
    12.9       NONE => lin_find_tree e t
   12.10     | x => x);
   12.11  
    13.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Feb 27 22:52:25 2010 +0100
    13.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Feb 27 23:13:01 2010 +0100
    13.3 @@ -51,9 +51,10 @@
    13.4  
    13.5  open Function_Lib
    13.6  
    13.7 -val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
    13.8 +val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord
    13.9  structure Term2tab = Table(type key = term * term val ord = term2_ord);
   13.10 -structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
   13.11 +structure Term3tab =
   13.12 +  Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord);
   13.13  
   13.14  (** Analyzing binary trees **)
   13.15  
    14.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Sat Feb 27 22:52:25 2010 +0100
    14.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sat Feb 27 23:13:01 2010 +0100
    14.3 @@ -689,7 +689,7 @@
    14.4    val cjs = conjs tm
    14.5    val  rawvars = fold_rev (fn eq => fn a =>
    14.6                                         grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs []
    14.7 -  val vars = sort (fn (x, y) => TermOrd.term_ord(term_of x,term_of y))
    14.8 +  val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y))
    14.9                    (distinct (op aconvc) rawvars)
   14.10   in (vars,map (grobify_equation vars) cjs)
   14.11   end;
   14.12 @@ -898,7 +898,7 @@
   14.13    val vars = filter (fn v => free_in v eq) evs
   14.14    val (qs,p) = isolate_monomials vars eq
   14.15    val rs = ideal (qs @ ps) p 
   14.16 -              (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
   14.17 +              (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t))
   14.18   in (eq, take (length qs) rs ~~ vars)
   14.19   end;
   14.20   fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
    15.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sat Feb 27 22:52:25 2010 +0100
    15.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sat Feb 27 23:13:01 2010 +0100
    15.3 @@ -636,7 +636,7 @@
    15.4  val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
    15.5                                addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
    15.6  
    15.7 -fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
    15.8 +fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
    15.9  
   15.10  fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
   15.11                                       {conv, dest_const, mk_const, is_const}) ord =
    16.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Feb 27 22:52:25 2010 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Feb 27 23:13:01 2010 +0100
    16.3 @@ -359,7 +359,7 @@
    16.4        not standard orelse T = nat_T orelse is_word_type T orelse
    16.5        exists (curry (op =) T o domain_type o type_of) sel_names
    16.6      val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    16.7 -                 |> sort TermOrd.typ_ord
    16.8 +                 |> sort Term_Ord.typ_ord
    16.9      val _ = if verbose andalso binary_ints = SOME true andalso
   16.10                 exists (member (op =) [nat_T, int_T]) all_Ts then
   16.11                print_v (K "The option \"binary_ints\" will be ignored because \
    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Feb 27 22:52:25 2010 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Feb 27 23:13:01 2010 +0100
    17.3 @@ -1122,7 +1122,7 @@
    17.4  
    17.5  (* term list -> (indexname * typ) list *)
    17.6  fun special_bounds ts =
    17.7 -  fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
    17.8 +  fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
    17.9  
   17.10  (* indexname * typ -> term -> term *)
   17.11  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 22:52:25 2010 +0100
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 23:13:01 2010 +0100
    18.3 @@ -103,7 +103,7 @@
    18.4               (case nice_term_ord (t11, t21) of
    18.5                  EQUAL => nice_term_ord (t12, t22)
    18.6                | ord => ord)
    18.7 -           | _ => TermOrd.fast_term_ord tp
    18.8 +           | _ => Term_Ord.fast_term_ord tp
    18.9  
   18.10  (* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
   18.11  fun tuple_list_for_name rel_table bounds name =
    19.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Feb 27 22:52:25 2010 +0100
    19.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Feb 27 23:13:01 2010 +0100
    19.3 @@ -400,13 +400,13 @@
    19.4    | name_ord (_, BoundName _) = GREATER
    19.5    | name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) =
    19.6      (case fast_string_ord (s1, s2) of
    19.7 -       EQUAL => TermOrd.typ_ord (T1, T2)
    19.8 +       EQUAL => Term_Ord.typ_ord (T1, T2)
    19.9       | ord => ord)
   19.10    | name_ord (FreeName _, _) = LESS
   19.11    | name_ord (_, FreeName _) = GREATER
   19.12    | name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) =
   19.13      (case fast_string_ord (s1, s2) of
   19.14 -       EQUAL => TermOrd.typ_ord (T1, T2)
   19.15 +       EQUAL => Term_Ord.typ_ord (T1, T2)
   19.16       | ord => ord)
   19.17    | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
   19.18  
    20.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Feb 27 22:52:25 2010 +0100
    20.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Feb 27 23:13:01 2010 +0100
    20.3 @@ -247,7 +247,7 @@
    20.4        let
    20.5          val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
    20.6          val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    20.7 -        val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
    20.8 +        val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last
    20.9        in
   20.10          list_comb (Const (s0, T --> T --> body_type T0),
   20.11                     map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
   20.12 @@ -815,7 +815,7 @@
   20.13        | call_sets [] uss vs = vs :: call_sets uss [] []
   20.14        | call_sets ([] :: _) _ _ = []
   20.15        | call_sets ((t :: ts) :: tss) uss vs =
   20.16 -        OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
   20.17 +        OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
   20.18      val sets = call_sets (fun_calls t [] []) [] []
   20.19      val indexed_sets = sets ~~ (index_seq 0 (length sets))
   20.20    in
   20.21 @@ -830,7 +830,7 @@
   20.22  (* hol_context -> styp -> term list -> (int * term option) list *)
   20.23  fun static_args_in_terms hol_ctxt x =
   20.24    map (static_args_in_term hol_ctxt x)
   20.25 -  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
   20.26 +  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
   20.27  
   20.28  (* (int * term option) list -> (int * term) list -> int list *)
   20.29  fun overlapping_indices [] _ = []
   20.30 @@ -882,7 +882,7 @@
   20.31                  val _ = not (null fixed_js) orelse raise SAME ()
   20.32                  val fixed_args = filter_indices fixed_js args
   20.33                  val vars = fold Term.add_vars fixed_args []
   20.34 -                           |> sort (TermOrd.fast_indexname_ord o pairself fst)
   20.35 +                           |> sort (Term_Ord.fast_indexname_ord o pairself fst)
   20.36                  val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
   20.37                                      fixed_args []
   20.38                                 |> sort int_ord
   20.39 @@ -972,7 +972,7 @@
   20.40      fun generality (js, _, _) = ~(length js)
   20.41      (* special_triple -> special_triple -> bool *)
   20.42      fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
   20.43 -      x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
   20.44 +      x1 <> x2 andalso OrdList.subset (prod_ord int_ord Term_Ord.term_ord)
   20.45                                        (j2 ~~ t2, j1 ~~ t1)
   20.46      (* typ -> special_triple list -> special_triple list -> special_triple list
   20.47         -> term list -> term list *)
    21.1 --- a/src/HOL/Tools/Qelim/langford.ML	Sat Feb 27 22:52:25 2010 +0100
    21.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Sat Feb 27 23:13:01 2010 +0100
    21.3 @@ -210,7 +210,7 @@
    21.4   let 
    21.5     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    21.6     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    21.7 -   val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
    21.8 +   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
    21.9     val p' = fold_rev gen ts p
   21.10   in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   21.11  
    22.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Sat Feb 27 22:52:25 2010 +0100
    22.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sat Feb 27 23:13:01 2010 +0100
    22.3 @@ -103,7 +103,7 @@
    22.4   let 
    22.5     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    22.6     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    22.7 -   val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
    22.8 +   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
    22.9     val p' = fold_rev gen ts p
   22.10   in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   22.11  
    23.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Feb 27 22:52:25 2010 +0100
    23.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Feb 27 23:13:01 2010 +0100
    23.3 @@ -80,7 +80,7 @@
    23.4  
    23.5  (*Express t as a product of (possibly) a numeral with other factors, sorted*)
    23.6  fun dest_coeff t =
    23.7 -    let val ts = sort TermOrd.term_ord (dest_prod t)
    23.8 +    let val ts = sort Term_Ord.term_ord (dest_prod t)
    23.9          val (n, _, ts') = find_first_numeral [] ts
   23.10                            handle TERM _ => (1, one, ts)
   23.11      in (n, mk_prod ts') end;
    24.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Feb 27 22:52:25 2010 +0100
    24.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Feb 27 23:13:01 2010 +0100
    24.3 @@ -74,7 +74,7 @@
    24.4  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    24.5  fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t
    24.6    | dest_coeff sign t =
    24.7 -    let val ts = sort TermOrd.term_ord (dest_prod t)
    24.8 +    let val ts = sort Term_Ord.term_ord (dest_prod t)
    24.9          val (n, ts') = find_first_numeral [] ts
   24.10                            handle TERM _ => (1, ts)
   24.11      in (sign*n, mk_prod (Term.fastype_of t) ts') end;
   24.12 @@ -124,12 +124,12 @@
   24.13      EQUAL => int_ord (Int.sign i, Int.sign j) 
   24.14    | ord => ord);
   24.15  
   24.16 -(*This resembles TermOrd.term_ord, but it puts binary numerals before other
   24.17 +(*This resembles Term_Ord.term_ord, but it puts binary numerals before other
   24.18    non-atomic terms.*)
   24.19  local open Term 
   24.20  in 
   24.21  fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
   24.22 -      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
   24.23 +      (case numterm_ord (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
   24.24    | numterm_ord
   24.25       (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
   24.26       num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
   24.27 @@ -139,7 +139,7 @@
   24.28        (case int_ord (size_of_term t, size_of_term u) of
   24.29          EQUAL =>
   24.30            let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   24.31 -            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
   24.32 +            (case Term_Ord.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
   24.33            end
   24.34        | ord => ord)
   24.35  and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    25.1 --- a/src/HOL/Tools/record.ML	Sat Feb 27 22:52:25 2010 +0100
    25.2 +++ b/src/HOL/Tools/record.ML	Sat Feb 27 23:13:01 2010 +0100
    25.3 @@ -1100,7 +1100,7 @@
    25.4  fun get_accupd_simps thy term defset =
    25.5    let
    25.6      val (acc, [body]) = strip_comb term;
    25.7 -    val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
    25.8 +    val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
    25.9      fun get_simp upd =
   25.10        let
   25.11          (* FIXME fresh "f" (!?) *)
    26.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Feb 27 22:52:25 2010 +0100
    26.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat Feb 27 23:13:01 2010 +0100
    26.3 @@ -320,7 +320,7 @@
    26.4  	(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
    26.5  	(* terms sorted in descending order, while only linear for terms      *)
    26.6  	(* sorted in ascending order                                          *)
    26.7 -	val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
    26.8 +	val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
    26.9  	val _ = if !trace_sat then
   26.10  			tracing ("Sorted non-trivial clauses:\n" ^
   26.11  			  cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
    27.1 --- a/src/Provers/Arith/cancel_factor.ML	Sat Feb 27 22:52:25 2010 +0100
    27.2 +++ b/src/Provers/Arith/cancel_factor.ML	Sat Feb 27 23:13:01 2010 +0100
    27.3 @@ -35,7 +35,7 @@
    27.4        if t aconv u then (u, k + 1) :: uks
    27.5        else (t, 1) :: (u, k) :: uks;
    27.6  
    27.7 -fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
    27.8 +fun count_terms ts = foldr ins_term (sort Term_Ord.term_ord ts, []);
    27.9  
   27.10  
   27.11  (* divide sum *)
    28.1 --- a/src/Provers/Arith/cancel_sums.ML	Sat Feb 27 22:52:25 2010 +0100
    28.2 +++ b/src/Provers/Arith/cancel_sums.ML	Sat Feb 27 23:13:01 2010 +0100
    28.3 @@ -37,11 +37,11 @@
    28.4  fun cons2 y (x, ys, z) = (x, y :: ys, z);
    28.5  fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
    28.6  
    28.7 -(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*)
    28.8 +(*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*)
    28.9  fun cancel ts [] vs = (ts, [], vs)
   28.10    | cancel [] us vs = ([], us, vs)
   28.11    | cancel (t :: ts) (u :: us) vs =
   28.12 -      (case TermOrd.term_ord (t, u) of
   28.13 +      (case Term_Ord.term_ord (t, u) of
   28.14          EQUAL => cancel ts us (t :: vs)
   28.15        | LESS => cons1 t (cancel ts (u :: us) vs)
   28.16        | GREATER => cons2 u (cancel (t :: ts) us vs));
   28.17 @@ -63,7 +63,7 @@
   28.18    | SOME bal =>
   28.19        let
   28.20          val thy = ProofContext.theory_of (Simplifier.the_context ss);
   28.21 -        val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal;
   28.22 +        val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal;
   28.23          val (ts', us', vs) = cancel ts us [];
   28.24        in
   28.25          if null vs then NONE
    29.1 --- a/src/Pure/Isar/rule_cases.ML	Sat Feb 27 22:52:25 2010 +0100
    29.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Feb 27 23:13:01 2010 +0100
    29.3 @@ -379,7 +379,7 @@
    29.4  local
    29.5  
    29.6  fun equal_cterms ts us =
    29.7 -  is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
    29.8 +  is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
    29.9  
   29.10  fun prep_rule n th =
   29.11    let
    30.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Feb 27 22:52:25 2010 +0100
    30.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Feb 27 23:13:01 2010 +0100
    30.3 @@ -364,7 +364,7 @@
    30.4  
    30.5  fun rem_thm_dups nicer xs =
    30.6    xs ~~ (1 upto length xs)
    30.7 -  |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
    30.8 +  |> sort (Term_Ord.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
    30.9    |> rem_cdups nicer
   30.10    |> sort (int_ord o pairself #2)
   30.11    |> map #1;
    31.1 --- a/src/Pure/envir.ML	Sat Feb 27 22:52:25 2010 +0100
    31.2 +++ b/src/Pure/envir.ML	Sat Feb 27 23:13:01 2010 +0100
    31.3 @@ -139,7 +139,7 @@
    31.4    (case t of
    31.5      Var (nT as (name', T)) =>
    31.6        if a = name' then env     (*cycle!*)
    31.7 -      else if TermOrd.indexname_ord (a, name') = LESS then
    31.8 +      else if Term_Ord.indexname_ord (a, name') = LESS then
    31.9          (case lookup (env, nT) of  (*if already assigned, chase*)
   31.10            NONE => update ((nT, Var (a, T)), env)
   31.11          | SOME u => vupdate ((aU, u), env))
    32.1 --- a/src/Pure/facts.ML	Sat Feb 27 22:52:25 2010 +0100
    32.2 +++ b/src/Pure/facts.ML	Sat Feb 27 23:13:01 2010 +0100
    32.3 @@ -171,7 +171,7 @@
    32.4  
    32.5  (* indexed props *)
    32.6  
    32.7 -val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of;
    32.8 +val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of;
    32.9  
   32.10  fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
   32.11  fun could_unify (Facts {props, ...}) = Net.unify_term props;
    33.1 --- a/src/Pure/meta_simplifier.ML	Sat Feb 27 22:52:25 2010 +0100
    33.2 +++ b/src/Pure/meta_simplifier.ML	Sat Feb 27 23:13:01 2010 +0100
    33.3 @@ -755,7 +755,7 @@
    33.4    mk_eq_True = K NONE,
    33.5    reorient = default_reorient};
    33.6  
    33.7 -val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
    33.8 +val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
    33.9  
   33.10  
   33.11  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
    34.1 --- a/src/Pure/more_thm.ML	Sat Feb 27 22:52:25 2010 +0100
    34.2 +++ b/src/Pure/more_thm.ML	Sat Feb 27 23:13:01 2010 +0100
    34.3 @@ -151,12 +151,12 @@
    34.4      val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
    34.5      val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
    34.6    in
    34.7 -    (case TermOrd.fast_term_ord (prop1, prop2) of
    34.8 +    (case Term_Ord.fast_term_ord (prop1, prop2) of
    34.9        EQUAL =>
   34.10 -        (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of
   34.11 +        (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of
   34.12            EQUAL =>
   34.13 -            (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of
   34.14 -              EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2)
   34.15 +            (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of
   34.16 +              EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2)
   34.17              | ord => ord)
   34.18          | ord => ord)
   34.19      | ord => ord)
   34.20 @@ -165,7 +165,7 @@
   34.21  
   34.22  (* tables and caches *)
   34.23  
   34.24 -structure Ctermtab = Table(type key = cterm val ord = TermOrd.fast_term_ord o pairself Thm.term_of);
   34.25 +structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o pairself Thm.term_of);
   34.26  structure Thmtab = Table(type key = thm val ord = thm_ord);
   34.27  
   34.28  fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
    35.1 --- a/src/Pure/old_term.ML	Sat Feb 27 22:52:25 2010 +0100
    35.2 +++ b/src/Pure/old_term.ML	Sat Feb 27 23:13:01 2010 +0100
    35.3 @@ -75,7 +75,7 @@
    35.4  
    35.5  (*Accumulates the Vars in the term, suppressing duplicates.*)
    35.6  fun add_term_vars (t, vars: term list) = case t of
    35.7 -    Var   _ => OrdList.insert TermOrd.term_ord t vars
    35.8 +    Var   _ => OrdList.insert Term_Ord.term_ord t vars
    35.9    | Abs (_,_,body) => add_term_vars(body,vars)
   35.10    | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   35.11    | _ => vars;
   35.12 @@ -84,7 +84,7 @@
   35.13  
   35.14  (*Accumulates the Frees in the term, suppressing duplicates.*)
   35.15  fun add_term_frees (t, frees: term list) = case t of
   35.16 -    Free   _ => OrdList.insert TermOrd.term_ord t frees
   35.17 +    Free   _ => OrdList.insert Term_Ord.term_ord t frees
   35.18    | Abs (_,_,body) => add_term_frees(body,frees)
   35.19    | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   35.20    | _ => frees;
    36.1 --- a/src/Pure/pattern.ML	Sat Feb 27 22:52:25 2010 +0100
    36.2 +++ b/src/Pure/pattern.ML	Sat Feb 27 23:13:01 2010 +0100
    36.3 @@ -226,7 +226,7 @@
    36.4                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    36.5                   in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
    36.6                   end;
    36.7 -  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
    36.8 +  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
    36.9  
   36.10  fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   36.11    if T = U then env
    37.1 --- a/src/Pure/proofterm.ML	Sat Feb 27 22:52:25 2010 +0100
    37.2 +++ b/src/Pure/proofterm.ML	Sat Feb 27 23:13:01 2010 +0100
    37.3 @@ -214,7 +214,7 @@
    37.4  
    37.5  (* proof body *)
    37.6  
    37.7 -val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
    37.8 +val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
    37.9  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
   37.10  
   37.11  val merge_oracles = OrdList.union oracle_ord;
    38.1 --- a/src/Pure/search.ML	Sat Feb 27 22:52:25 2010 +0100
    38.2 +++ b/src/Pure/search.ML	Sat Feb 27 23:13:01 2010 +0100
    38.3 @@ -197,7 +197,7 @@
    38.4  structure Thm_Heap = Heap
    38.5  (
    38.6    type elem = int * thm;
    38.7 -  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of);
    38.8 +  val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of);
    38.9  );
   38.10  
   38.11  val trace_BEST_FIRST = Unsynchronized.ref false;
    39.1 --- a/src/Pure/sorts.ML	Sat Feb 27 22:52:25 2010 +0100
    39.2 +++ b/src/Pure/sorts.ML	Sat Feb 27 23:13:01 2010 +0100
    39.3 @@ -71,13 +71,13 @@
    39.4  
    39.5  (** ordered lists of sorts **)
    39.6  
    39.7 -val make = OrdList.make TermOrd.sort_ord;
    39.8 -val subset = OrdList.subset TermOrd.sort_ord;
    39.9 -val union = OrdList.union TermOrd.sort_ord;
   39.10 -val subtract = OrdList.subtract TermOrd.sort_ord;
   39.11 +val make = OrdList.make Term_Ord.sort_ord;
   39.12 +val subset = OrdList.subset Term_Ord.sort_ord;
   39.13 +val union = OrdList.union Term_Ord.sort_ord;
   39.14 +val subtract = OrdList.subtract Term_Ord.sort_ord;
   39.15  
   39.16 -val remove_sort = OrdList.remove TermOrd.sort_ord;
   39.17 -val insert_sort = OrdList.insert TermOrd.sort_ord;
   39.18 +val remove_sort = OrdList.remove Term_Ord.sort_ord;
   39.19 +val insert_sort = OrdList.insert Term_Ord.sort_ord;
   39.20  
   39.21  fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   39.22    | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
    40.1 --- a/src/Pure/term_ord.ML	Sat Feb 27 22:52:25 2010 +0100
    40.2 +++ b/src/Pure/term_ord.ML	Sat Feb 27 23:13:01 2010 +0100
    40.3 @@ -29,7 +29,7 @@
    40.4    val term_cache: (term -> 'a) -> term -> 'a
    40.5  end;
    40.6  
    40.7 -structure TermOrd: TERM_ORD =
    40.8 +structure Term_Ord: TERM_ORD =
    40.9  struct
   40.10  
   40.11  (* fast syntactic ordering -- tuned for inequalities *)
   40.12 @@ -223,11 +223,11 @@
   40.13  
   40.14  end;
   40.15  
   40.16 -structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
   40.17 +structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
   40.18  open Basic_Term_Ord;
   40.19  
   40.20 -structure Var_Graph = Graph(type key = indexname val ord = TermOrd.fast_indexname_ord);
   40.21 -structure Sort_Graph = Graph(type key = sort val ord = TermOrd.sort_ord);
   40.22 -structure Typ_Graph = Graph(type key = typ val ord = TermOrd.typ_ord);
   40.23 -structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
   40.24 +structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
   40.25 +structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
   40.26 +structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
   40.27 +structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
   40.28  
    41.1 --- a/src/Pure/term_subst.ML	Sat Feb 27 22:52:25 2010 +0100
    41.2 +++ b/src/Pure/term_subst.ML	Sat Feb 27 23:13:01 2010 +0100
    41.3 @@ -198,9 +198,9 @@
    41.4  
    41.5  fun zero_var_indexes_inst ts =
    41.6    let
    41.7 -    val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []);
    41.8 +    val tvars = sort Term_Ord.tvar_ord (fold Term.add_tvars ts []);
    41.9      val instT = map (apsnd TVar) (zero_var_inst tvars);
   41.10 -    val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
   41.11 +    val vars = sort Term_Ord.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
   41.12      val inst = map (apsnd Var) (zero_var_inst vars);
   41.13    in (instT, inst) end;
   41.14  
    42.1 --- a/src/Pure/thm.ML	Sat Feb 27 22:52:25 2010 +0100
    42.2 +++ b/src/Pure/thm.ML	Sat Feb 27 23:13:01 2010 +0100
    42.3 @@ -384,9 +384,9 @@
    42.4  
    42.5  fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
    42.6  
    42.7 -val union_hyps = OrdList.union TermOrd.fast_term_ord;
    42.8 -val insert_hyps = OrdList.insert TermOrd.fast_term_ord;
    42.9 -val remove_hyps = OrdList.remove TermOrd.fast_term_ord;
   42.10 +val union_hyps = OrdList.union Term_Ord.fast_term_ord;
   42.11 +val insert_hyps = OrdList.insert Term_Ord.fast_term_ord;
   42.12 +val remove_hyps = OrdList.remove Term_Ord.fast_term_ord;
   42.13  
   42.14  
   42.15  (* merge theories of cterms/thms -- trivial absorption only *)
    43.1 --- a/src/Pure/unify.ML	Sat Feb 27 22:52:25 2010 +0100
    43.2 +++ b/src/Pure/unify.ML	Sat Feb 27 23:13:01 2010 +0100
    43.3 @@ -558,7 +558,7 @@
    43.4    if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
    43.5        if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
    43.6        else raise TERM ("add_ffpair: Var name confusion", [t,u])
    43.7 -  else if TermOrd.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
    43.8 +  else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
    43.9         clean_ffpair thy ((rbinder, u, t), (env,tpairs))
   43.10          else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
   43.11      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
    44.1 --- a/src/Tools/Compute_Oracle/linker.ML	Sat Feb 27 22:52:25 2010 +0100
    44.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Sat Feb 27 23:13:01 2010 +0100
    44.3 @@ -50,7 +50,7 @@
    44.4    | constant_of _ = raise Link "constant_of"
    44.5  
    44.6  fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
    44.7 -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))
    44.8 +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))
    44.9  fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
   44.10  
   44.11  
   44.12 @@ -70,7 +70,7 @@
   44.13      handle Type.TYPE_MATCH => NONE
   44.14  
   44.15  fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
   44.16 -    (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
   44.17 +    (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)
   44.18  
   44.19  structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
   44.20  
   44.21 @@ -380,7 +380,7 @@
   44.22          ComputeThm (hyps, shyps, prop)
   44.23      end
   44.24  
   44.25 -val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord
   44.26 +val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
   44.27  
   44.28  fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
   44.29  
    45.1 --- a/src/ZF/arith_data.ML	Sat Feb 27 22:52:25 2010 +0100
    45.2 +++ b/src/ZF/arith_data.ML	Sat Feb 27 23:13:01 2010 +0100
    45.3 @@ -104,7 +104,7 @@
    45.4  
    45.5  (*Dummy version: the "coefficient" is always 1.
    45.6    In the result, the factors are sorted terms*)
    45.7 -fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
    45.8 +fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t)));
    45.9  
   45.10  (*Find first coefficient-term THAT MATCHES u*)
   45.11  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    46.1 --- a/src/ZF/int_arith.ML	Sat Feb 27 22:52:25 2010 +0100
    46.2 +++ b/src/ZF/int_arith.ML	Sat Feb 27 23:13:01 2010 +0100
    46.3 @@ -95,7 +95,7 @@
    46.4  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    46.5  fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
    46.6    | dest_coeff sign t =
    46.7 -    let val ts = sort TermOrd.term_ord (dest_prod t)
    46.8 +    let val ts = sort Term_Ord.term_ord (dest_prod t)
    46.9          val (n, ts') = find_first_numeral [] ts
   46.10                            handle TERM _ => (1, ts)
   46.11      in (sign*n, mk_prod ts') end;