# HG changeset patch
# User wenzelm
# Date 1230733810 -3600
# Node ID 5c25a20129754778c16fa8d9b74ae9d2f687d0cf
# Parent  6aefc5ff8e6379c36ae690052d8cb17643533aff
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

diff -r 6aefc5ff8e63 -r 5c25a2012975 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/CCL/Wfd.thy	Wed Dec 31 15:30:10 2008 +0100
@@ -434,9 +434,9 @@
   | get_bno l n (Bound m) = (m-length(l),n)
 
 (* Not a great way of identifying induction hypothesis! *)
-fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse
-                 could_unify(x,hd (prems_of @{thm rcall2T})) orelse
-                 could_unify(x,hd (prems_of @{thm rcall3T}))
+fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse
+                 Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse
+                 Term.could_unify(x,hd (prems_of @{thm rcall3T}))
 
 fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
   let val bvs = bvars Bi []
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/FOLP/IFOLP.thy	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/IFOLP.thy
-    ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
@@ -247,7 +246,7 @@
           and concl = discard_proof (Logic.strip_assums_concl prem)
       in
           if exists (fn hyp => hyp aconv concl) hyps
-          then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
+          then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
                    [_] => assume_tac i
                  |  _  => no_tac
           else no_tac
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Dec 31 15:30:10 2008 +0100
@@ -1,8 +1,7 @@
-(*
-  Title:     The algebraic hierarchy of rings as axiomatic classes
-  Id:        $Id$
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:     HOL/Algebra/abstract/Ring2.thy
+    Author:    Clemens Ballarin
+
+The algebraic hierarchy of rings as axiomatic classes.
 *)
 
 header {* The algebraic hierarchy of rings as type classes *}
@@ -211,7 +210,7 @@
         @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
   | ring_ord _ = ~1;
 
-fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
+fun termless_ring (a, b) = (TermOrd.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",
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,4 @@
-(*
-  Id:        $Id$
-  Author:    Clemens Ballarin
+(*  Author:    Clemens Ballarin
 
 Normalisation method for locales ring and cring.
 *)
@@ -48,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) = (Term.term_lpo ord (a, b) = LESS);
+    fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
   in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
 
 fun algebra_tac ctxt =
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -353,7 +353,7 @@
 
 fun equals_fun thy assume t =
     case t of
-        Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+        Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
       | _ => NONE
 
 fun eta_expand thy assumes origt =
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/OrderedGroup.thy	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:   HOL/OrderedGroup.thy
-    ID:      $Id$
-    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
-             with contributions by Jeremy Avigad
+    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
 *)
 
 header {* Ordered Groups *}
@@ -1376,7 +1374,7 @@
         @{const_name HOL.uminus}, @{const_name HOL.minus}]
   | agrp_ord _ = ~1;
 
-fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
+fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
 
 local
   val ac1 = mk_meta_eq @{thm add_assoc};
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
-(*  Title:      DistinctTreeProver.thy
-    ID:         $Id$
+(*  Title:      HOL/Statespace/DistinctTreeProver.thy
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -646,9 +645,9 @@
 val const_decls = map (fn i => Syntax.no_syn 
                                  ("const" ^ string_of_int i,Type ("nat",[]))) nums
 
-val consts = sort Term.fast_term_ord 
+val consts = sort TermOrd.fast_term_ord 
               (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort Term.fast_term_ord 
+val consts' = sort TermOrd.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
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
-(*  Title:      distinct_tree_prover.thy
-    ID:         $Id$
+(*  Title:      HOL/Statespace/distinct_tree_prover.ML
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -83,7 +82,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 Term.fast_term_ord e t of
+  (case bin_find_tree TermOrd.fast_term_ord e t of
      NONE => lin_find_tree e t
    | x => x);
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -599,14 +598,14 @@
      if length ideal = 2 then ideal else [eq_commute, eq_commute]
   val ring_dest_neg =
     fn t => let val (l,r) = dest_comb t in
-        if could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
+        if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
       end
 
  val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
 (*
  fun ring_dest_inv t =
     let val (l,r) = dest_comb t in
-        if could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
+        if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
     end
 *)
  val ring_dest_add = dest_binary ring_add_tm;
@@ -687,7 +686,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) => Term.term_ord(term_of x,term_of y))
+  val vars = sort (fn (x, y) => TermOrd.term_ord(term_of x,term_of y))
                   (distinct (op aconvc) rawvars)
  in (vars,map (grobify_equation vars) cjs)
  end;
@@ -896,7 +895,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) => Term.term_ord (term_of s, term_of t))
+              (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
  in (eq,Library.take (length qs, rs) ~~ vars)
  end;
  fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -615,7 +614,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 add_0}, @{thm add_Suc}];
 
-fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS;
+fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
 
 fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
                                      {conv, dest_const, mk_const, is_const}) ord =
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/Qelim/langford.ML
--- a/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,3 +1,7 @@
+(*  Title:      HOL/Tools/Qelim/langford.ML
+    Author:     Amine Chaieb, TU Muenchen
+*)
+
 signature LANGFORD_QE = 
 sig
   val dlo_tac : Proof.context -> int -> tactic
@@ -211,7 +215,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) => Term.fast_term_ord (term_of a, term_of b)) (f p)
+   val ts = sort (fn (a,b) => TermOrd.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));
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 15:30:10 2008 +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) => Term.fast_term_ord (term_of a, term_of b)) (f p)
+   val ts = sort (fn (a,b) => TermOrd.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));
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/function_package/decompose.ML
--- a/src/HOL/Tools/function_package/decompose.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/function_package/decompose.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -19,7 +19,7 @@
 structure Decompose : DECOMPOSE =
 struct
 
-structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
+structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
 
 
 fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/function_package/termination.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,4 +1,4 @@
-(*  Title:       HOL/Tools/function_package/termination_data.ML
+(*  Title:       HOL/Tools/function_package/termination.ML
     Author:      Alexander Krauss, TU Muenchen
 
 Context data for termination proofs
@@ -50,9 +50,9 @@
 
 open FundefLib
 
-val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
+val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
 structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
-structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
+structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
 
 (** Analyzing binary trees **)
 
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;
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/nat_simprocs.ML
--- a/src/HOL/Tools/nat_simprocs.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
-(*  Title:      HOL/nat_simprocs.ML
-    ID:         $Id$
+(*  Title:      HOL/Tools/nat_simprocs.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
 
 Simprocs for nat numerals.
 *)
@@ -81,7 +79,7 @@
 
 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
 fun dest_coeff 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, one, ts)
     in (n, mk_prod ts') end;
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,6 @@
 (*  Title:      HOL/Tools/sat_funcs.ML
-    ID:         $Id$
     Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
-    Author:     Tjark Weber
-    Copyright   2005-2006
-
+    Author:     Tjark Weber, TU Muenchen
 
 Proof reconstruction from SAT solvers.
 
@@ -323,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 (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
+	val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
 	val _ = if !trace_sat then
 			tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
 		else ()
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/ex/reflection.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,19 +1,18 @@
-(*
-    ID:         $Id$
-    Author:     Amine Chaieb, TU Muenchen
+(*  Author:     Amine Chaieb, TU Muenchen
 
 A trial for automatical reification.
 *)
 
-signature REFLECTION = sig
+signature REFLECTION =
+sig
   val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
   val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
   val gen_reflection_tac: Proof.context -> (cterm -> thm)
     -> thm list -> thm list -> term option -> int -> tactic
 end;
 
-structure Reflection : REFLECTION
-= struct
+structure Reflection : REFLECTION =
+struct
 
 val ext2 = thm "ext2";
 val nth_Cons_0 = thm "nth_Cons_0";
@@ -38,7 +37,7 @@
    val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
    fun add_fterms (t as t1 $ t2) = 
-       if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
+       if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
        else add_fterms t1 #> add_fterms t2
      | add_fterms (t as Abs(xn,xT,t')) = 
        if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
@@ -139,7 +138,7 @@
         val (tyenv, tmenv) =
         Pattern.match thy
         ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
-        (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
+        (Envir.type_env (Envir.empty 0), Vartab.empty)
         val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
         val (fts,its) = 
 	    (map (snd o snd) fnvs,
@@ -191,7 +190,7 @@
    val rhs_P = subst_free subst rhs
    val (tyenv, tmenv) = Pattern.match 
 	                    thy (rhs_P, t)
-	                    (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
+	                    (Envir.type_env (Envir.empty 0), Vartab.empty)
    val sbst = Envir.subst_vars (tyenv, tmenv)
    val sbsT = Envir.typ_subst_TVars tyenv
    val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Provers/Arith/cancel_factor.ML
--- a/src/Provers/Arith/cancel_factor.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/Arith/cancel_factor.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/cancel_factor.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
@@ -36,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 Term.term_ord ts, []);
+fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
 
 
 (* divide sum *)
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Provers/Arith/cancel_sums.ML
--- a/src/Provers/Arith/cancel_sums.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/Arith/cancel_sums.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/cancel_sums.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Cancel common summands of balanced expressions:
@@ -38,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. Logic.term_ord*)
+(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*)
 fun cancel ts [] vs = (ts, [], vs)
   | cancel [] us vs = ([], us, vs)
   | cancel (t :: ts) (u :: us) vs =
-      (case Term.term_ord (t, u) of
+      (case TermOrd.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));
@@ -64,7 +63,7 @@
   | SOME bal =>
       let
         val thy = ProofContext.theory_of (Simplifier.the_context ss);
-        val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
+        val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal;
         val (ts', us', vs) = cancel ts us [];
       in
         if null vs then NONE
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/eqsubst.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,13 +1,12 @@
 (*  Title:      Provers/eqsubst.ML
-    ID:         $Id$
-    Author:     Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
+    Author:     Lucas Dixon, University of Edinburgh
 
 A proof method to perform a substiution using an equation.
 *)
 
 signature EQSUBST =
 sig
-  (* a type abriviation for match information *)
+  (* a type abbreviation for match information *)
   type match =
        ((indexname * (sort * typ)) list (* type instantiations *)
         * (indexname * (typ * term)) list) (* term instantiations *)
@@ -224,7 +223,7 @@
       (* is it OK to ignore the type instantiation info?
          or should I be using it? *)
       val typs_unify =
-          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
+          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
             handle Type.TUNIFY => NONE;
     in
       case typs_unify of
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/IsaMakefile	Wed Dec 31 15:30:10 2008 +0100
@@ -82,8 +82,8 @@
   logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
   old_goals.ML old_term.ML pattern.ML primitive_defs.ML proofterm.ML	\
   pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML	\
-  subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
-  thm.ML type.ML type_infer.ML unify.ML variable.ML			\
+  subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML	\
+  theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML		\
   ../Tools/quickcheck.ML
 	@./mk
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/find_theorems.ML
-    ID:         $Id$
     Author:     Rafal Kolanski and Gerwin Klein, NICTA
 
 Retrieve theorems from proof context.
@@ -287,7 +286,7 @@
 
 fun rem_thm_dups xs =
   xs ~~ (1 upto length xs)
-  |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
+  |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
   |> rem_cdups
   |> sort (int_ord o pairself #2)
   |> map #1;
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Pure/Isar/locale.ML
-    ID:         $Id$
-    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
+    Author:     Clemens Ballarin, TU Muenchen
+    Author:     Markus Wenzel, LMU/TU Muenchen
 
 Locales -- Isar proof contexts as meta-level predicates, with local
 syntax and implicit structures.
@@ -1297,7 +1297,7 @@
 
 fun defs_ord (defs1, defs2) =
     list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
-      Term.fast_term_ord (d1, d2)) (defs1, defs2);
+      TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
 structure Defstab =
     TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/rule_cases.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Annotations and local contexts of rules.
@@ -319,7 +318,7 @@
 local
 
 fun equal_cterms ts us =
-  is_equal (list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us));
+  is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
 
 fun prep_rule n th =
   let
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/ROOT.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -25,6 +25,7 @@
 (*fundamental structures*)
 use "name.ML";
 use "term.ML";
+use "term_ord.ML";
 use "term_subst.ML";
 use "old_term.ML";
 use "logic.ML";
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/envir.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      Pure/envir.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1988  University of Cambridge
 
 Environments.  The type of a term variable / sort of a type variable is
 part of its name. The lookup function must apply type substitutions,
@@ -118,7 +116,7 @@
 fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
       Var (nT as (name', T)) =>
         if a = name' then env     (*cycle!*)
-        else if Term.indexname_ord (a, name') = LESS then
+        else if TermOrd.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))
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/facts.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/facts.ML
-    ID:         $Id$
     Author:     Makarius
 
 Environment of named facts, optionally indexed by proposition.
@@ -166,7 +165,7 @@
 
 (* indexed props *)
 
-val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
+val prop_ord = TermOrd.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;
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/meta_simplifier.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow and Stefan Berghofer
+    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
 
 Meta-level Simplification.
 *)
@@ -788,7 +787,7 @@
   mk_eq_True = K NONE,
   reorient = default_reorient};
 
-val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
+val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
 
 
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/more_thm.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/more_thm.ML
-    ID:         $Id$
     Author:     Makarius
 
 Further operations on type ctyp/cterm/thm, outside the inference kernel.
@@ -128,12 +127,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 Term.fast_term_ord (prop1, prop2) of
+    (case TermOrd.fast_term_ord (prop1, prop2) of
       EQUAL =>
-        (case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of
+        (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of
           EQUAL =>
-            (case list_ord Term.fast_term_ord (hyps1, hyps2) of
-              EQUAL => list_ord Term.sort_ord (shyps1, shyps2)
+            (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of
+              EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2)
             | ord => ord)
         | ord => ord)
     | ord => ord)
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/old_term.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -17,7 +17,7 @@
 
 (*Accumulates the Vars in the term, suppressing duplicates*)
 fun add_term_vars (t, vars: term list) = case t of
-    Var   _ => OrdList.insert Term.term_ord t vars
+    Var   _ => OrdList.insert TermOrd.term_ord t vars
   | Abs (_,_,body) => add_term_vars(body,vars)
   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   | _ => vars;
@@ -26,7 +26,7 @@
 
 (*Accumulates the Frees in the term, suppressing duplicates*)
 fun add_term_frees (t, frees: term list) = case t of
-    Free   _ => OrdList.insert Term.term_ord t frees
+    Free   _ => OrdList.insert TermOrd.term_ord t frees
   | Abs (_,_,body) => add_term_frees(body,frees)
   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   | _ => frees;
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/pattern.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/pattern.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer
+    Author:     Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen
 
 Unification of Higher-Order Patterns.
 
@@ -223,7 +222,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 Term.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) 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
 
 fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/proofterm.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -188,7 +188,7 @@
 
 (* proof body *)
 
-val oracle_ord = prod_ord fast_string_ord Term.fast_term_ord;
+val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
 fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
 
 fun make_body prf =
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/search.ML
--- a/src/Pure/search.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/search.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/search.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson and Norbert Voelker
 
 Search tacticals.
@@ -42,10 +41,8 @@
 (** Instantiation of heaps for best-first search **)
 
 (*total ordering on theorems, allowing duplicates to be found*)
-structure ThmHeap =
-  HeapFun (type elem = int * thm
-    val ord = Library.prod_ord Library.int_ord
-      (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
+structure ThmHeap = HeapFun(type elem = int * thm
+  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of));
 
 
 structure Search : SEARCH =
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/sorts.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/sorts.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 The order-sorted algebra of type classes.
@@ -74,13 +73,13 @@
 
 (** ordered lists of sorts **)
 
-val make = OrdList.make Term.sort_ord;
-val op subset = OrdList.subset Term.sort_ord;
-val op union = OrdList.union Term.sort_ord;
-val subtract = OrdList.subtract Term.sort_ord;
+val make = OrdList.make TermOrd.sort_ord;
+val op subset = OrdList.subset TermOrd.sort_ord;
+val op union = OrdList.union TermOrd.sort_ord;
+val subtract = OrdList.subtract TermOrd.sort_ord;
 
-val remove_sort = OrdList.remove Term.sort_ord;
-val insert_sort = OrdList.insert Term.sort_ord;
+val remove_sort = OrdList.remove TermOrd.sort_ord;
+val insert_sort = OrdList.insert TermOrd.sort_ord;
 
 fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/term.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -76,9 +76,6 @@
   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   val add_term_names: term * string list -> string list
   val aconv: term * term -> bool
-  structure Vartab: TABLE
-  structure Typtab: TABLE
-  structure Termtab: TABLE
   val propT: typ
   val strip_all_body: term -> term
   val strip_all_vars: term -> (string * typ) list
@@ -92,8 +89,6 @@
   val subst_bound: term * term -> term
   val betapply: term * term -> term
   val betapplys: term * term list -> term
-  val eq_ix: indexname * indexname -> bool
-  val could_unify: term * term -> bool
   val subst_free: (term * term) list -> term -> term
   val abstract_over: term * term -> term
   val lambda: term -> term -> term
@@ -156,23 +151,14 @@
   val add_free_names: term -> string list -> string list
   val add_frees: term -> (string * typ) list -> (string * typ) list
   val hidden_polymorphism: term -> (indexname * sort) list
+  val eq_ix: indexname * indexname -> bool
+  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
+  val eq_var: (indexname * typ) * (indexname * typ) -> bool
+  val could_unify: term * term -> bool
   val strip_abs_eta: int -> term -> (string * typ) list * term
-  val fast_indexname_ord: indexname * indexname -> order
-  val indexname_ord: indexname * indexname -> order
-  val sort_ord: sort * sort -> order
-  val typ_ord: typ * typ -> order
-  val fast_term_ord: term * term -> order
-  val term_ord: term * term -> order
-  val hd_ord: term * term -> order
-  val termless: term * term -> bool
-  val term_lpo: (term -> int) -> term * term -> order
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val map_abs_vars: (string -> string) -> term -> term
   val rename_abs: term -> term -> term -> term option
-  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
-  val eq_var: (indexname * typ) * (indexname * typ) -> bool
-  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
-  val var_ord: (indexname * typ) * (indexname * typ) -> order
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
   val maxidx_typs: typ list -> int -> int
@@ -514,9 +500,17 @@
 
 
 
-(** Comparing terms, types, sorts etc. **)
+(** Comparing terms **)
+
+(* variables *)
+
+fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
 
-(* alpha equivalence -- tuned for equalities *)
+fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
+fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
+
+
+(* alpha equivalence *)
 
 fun tm1 aconv tm2 =
   pointer_eq (tm1, tm2) orelse
@@ -526,184 +520,24 @@
     | (a1, a2) => a1 = a2);
 
 
-(* fast syntactic ordering -- tuned for inequalities *)
-
-fun fast_indexname_ord ((x, i), (y, j)) =
-  (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
-
-fun sort_ord SS =
-  if pointer_eq SS then EQUAL
-  else dict_ord fast_string_ord SS;
-
-local
-
-fun cons_nr (TVar _) = 0
-  | cons_nr (TFree _) = 1
-  | cons_nr (Type _) = 2;
-
-in
-
-fun typ_ord TU =
-  if pointer_eq TU then EQUAL
-  else
-    (case TU of
-      (Type (a, Ts), Type (b, Us)) =>
-        (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
-    | (TFree (a, S), TFree (b, S')) =>
-        (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
-    | (TVar (xi, S), TVar (yj, S')) =>
-        (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
-    | (T, U) => int_ord (cons_nr T, cons_nr U));
-
-end;
-
-local
-
-fun cons_nr (Const _) = 0
-  | cons_nr (Free _) = 1
-  | cons_nr (Var _) = 2
-  | cons_nr (Bound _) = 3
-  | cons_nr (Abs _) = 4
-  | cons_nr (_ $ _) = 5;
-
-fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
-  | struct_ord (t1 $ t2, u1 $ u2) =
-      (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
-  | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
-
-fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
-  | atoms_ord (t1 $ t2, u1 $ u2) =
-      (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
-  | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
-  | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
-  | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
-  | atoms_ord (Bound i, Bound j) = int_ord (i, j)
-  | atoms_ord _ = sys_error "atoms_ord";
-
-fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
-      (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
-  | types_ord (t1 $ t2, u1 $ u2) =
-      (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
-  | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
-  | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
-  | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
-  | types_ord (Bound _, Bound _) = EQUAL
-  | types_ord _ = sys_error "types_ord";
-
-in
-
-fun fast_term_ord tu =
-  if pointer_eq tu then EQUAL
-  else
-    (case struct_ord tu of
-      EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
-    | ord => ord);
-
-structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
-structure Typtab = TableFun(type key = typ val ord = typ_ord);
-structure Termtab = TableFun(type key = term val ord = fast_term_ord);
-
-end;
-
-
-(* term_ord *)
-
-(*a linear well-founded AC-compatible ordering for terms:
-  s < t <=> 1. size(s) < size(t) or
-            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
-            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
-               (s1..sn) < (t1..tn) (lexicographically)*)
+(*A fast unification filter: true unless the two terms cannot be unified.
+  Terms must be NORMAL.  Treats all Vars as distinct. *)
+fun could_unify (t, u) =
+  let
+    fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
+      | matchrands _ _ = true;
+  in
+    case (head_of t, head_of u) of
+      (_, Var _) => true
+    | (Var _, _) => true
+    | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
+    | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
+    | (Bound i, Bound j) => i = j andalso matchrands t u
+    | (Abs _, _) => true   (*because of possible eta equality*)
+    | (_, Abs _) => true
+    | _ => false
+  end;
 
-fun indexname_ord ((x, i), (y, j)) =
-  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
-
-local
-
-fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
-  | hd_depth p = p;
-
-fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
-  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
-  | dest_hd (Var v) = (v, 2)
-  | dest_hd (Bound i) = ((("", i), dummyT), 3)
-  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
-
-in
-
-fun term_ord tu =
-  if pointer_eq tu then EQUAL
-  else
-    (case tu of
-      (Abs (_, T, t), Abs(_, U, u)) =>
-        (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
-    | (t, u) =>
-        (case int_ord (size_of_term t, size_of_term u) of
-          EQUAL =>
-            (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
-              EQUAL => args_ord (t, u) | ord => ord)
-        | ord => ord))
-and hd_ord (f, g) =
-  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
-and args_ord (f $ t, g $ u) =
-      (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
-  | args_ord _ = EQUAL;
-
-fun termless tu = (term_ord tu = LESS);
-
-end;
-
-
-(** Lexicographic path order on terms **)
-
-(*
-  See Baader & Nipkow, Term rewriting, CUP 1998.
-  Without variables.  Const, Var, Bound, Free and Abs are treated all as
-  constants.
-
-  f_ord maps terms to integers and serves two purposes:
-  - Predicate on constant symbols.  Those that are not recognised by f_ord
-    must be mapped to ~1.
-  - Order on the recognised symbols.  These must be mapped to distinct
-    integers >= 0.
-  The argument of f_ord is never an application.
-*)
-
-local
-
-fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
-  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
-  | unrecognized (Var v) = ((1, v), 1)
-  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
-  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
-
-fun dest_hd f_ord t =
-  let val ord = f_ord t
-  in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
-
-fun term_lpo f_ord (s, t) =
-  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
-    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
-    then case hd_ord f_ord (f, g) of
-        GREATER =>
-          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
-          then GREATER else LESS
-      | EQUAL =>
-          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
-          then list_ord (term_lpo f_ord) (ss, ts)
-          else LESS
-      | LESS => LESS
-    else GREATER
-  end
-and hd_ord f_ord (f, g) = case (f, g) of
-    (Abs (_, T, t), Abs (_, U, u)) =>
-      (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
-  | (_, _) => prod_ord (prod_ord int_ord
-                  (prod_ord indexname_ord typ_ord)) int_ord
-                (dest_hd f_ord f, dest_hd f_ord g);
-
-in
-val term_lpo = term_lpo
-end;
 
 
 (** Connectives of higher order logic **)
@@ -854,35 +688,6 @@
   in (vs1 @ vs2, t'') end;
 
 
-(* comparing variables *)
-
-fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
-
-fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
-fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
-
-val tvar_ord = prod_ord indexname_ord sort_ord;
-val var_ord = prod_ord indexname_ord typ_ord;
-
-
-(*A fast unification filter: true unless the two terms cannot be unified.
-  Terms must be NORMAL.  Treats all Vars as distinct. *)
-fun could_unify (t, u) =
-  let
-    fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
-      | matchrands _ _ = true;
-  in
-    case (head_of t, head_of u) of
-      (_, Var _) => true
-    | (Var _, _) => true
-    | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
-    | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
-    | (Bound i, Bound j) => i = j andalso matchrands t u
-    | (Abs _, _) => true   (*because of possible eta equality*)
-    | (_, Abs _) => true
-    | _ => false
-  end;
-
 (*Substitute new for free occurrences of old in a term*)
 fun subst_free [] = I
   | subst_free pairs =
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/term_ord.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_ord.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -0,0 +1,209 @@
+(*  Title:      Pure/term_ord.ML
+    Author:     Tobias Nipkow and Makarius, TU Muenchen
+
+Term orderings.
+*)
+
+signature TERM_ORD =
+sig
+  val fast_indexname_ord: indexname * indexname -> order
+  val sort_ord: sort * sort -> order
+  val typ_ord: typ * typ -> order
+  val fast_term_ord: term * term -> order
+  val indexname_ord: indexname * indexname -> order
+  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
+  val var_ord: (indexname * typ) * (indexname * typ) -> order
+  val term_ord: term * term -> order
+  val hd_ord: term * term -> order
+  val termless: term * term -> bool
+  val term_lpo: (term -> int) -> term * term -> order
+end;
+
+structure TermOrd: TERM_ORD =
+struct
+
+(* fast syntactic ordering -- tuned for inequalities *)
+
+fun fast_indexname_ord ((x, i), (y, j)) =
+  (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
+
+fun sort_ord SS =
+  if pointer_eq SS then EQUAL
+  else dict_ord fast_string_ord SS;
+
+local
+
+fun cons_nr (TVar _) = 0
+  | cons_nr (TFree _) = 1
+  | cons_nr (Type _) = 2;
+
+in
+
+fun typ_ord TU =
+  if pointer_eq TU then EQUAL
+  else
+    (case TU of
+      (Type (a, Ts), Type (b, Us)) =>
+        (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
+    | (TFree (a, S), TFree (b, S')) =>
+        (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
+    | (TVar (xi, S), TVar (yj, S')) =>
+        (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
+    | (T, U) => int_ord (cons_nr T, cons_nr U));
+
+end;
+
+local
+
+fun cons_nr (Const _) = 0
+  | cons_nr (Free _) = 1
+  | cons_nr (Var _) = 2
+  | cons_nr (Bound _) = 3
+  | cons_nr (Abs _) = 4
+  | cons_nr (_ $ _) = 5;
+
+fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
+  | struct_ord (t1 $ t2, u1 $ u2) =
+      (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
+  | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
+
+fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
+  | atoms_ord (t1 $ t2, u1 $ u2) =
+      (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
+  | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
+  | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
+  | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
+  | atoms_ord (Bound i, Bound j) = int_ord (i, j)
+  | atoms_ord _ = sys_error "atoms_ord";
+
+fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
+      (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
+  | types_ord (t1 $ t2, u1 $ u2) =
+      (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
+  | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
+  | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
+  | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
+  | types_ord (Bound _, Bound _) = EQUAL
+  | types_ord _ = sys_error "types_ord";
+
+in
+
+fun fast_term_ord tu =
+  if pointer_eq tu then EQUAL
+  else
+    (case struct_ord tu of
+      EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
+    | ord => ord);
+
+end;
+
+
+(* term_ord *)
+
+(*a linear well-founded AC-compatible ordering for terms:
+  s < t <=> 1. size(s) < size(t) or
+            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
+            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
+               (s1..sn) < (t1..tn) (lexicographically)*)
+
+fun indexname_ord ((x, i), (y, j)) =
+  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
+
+val tvar_ord = prod_ord indexname_ord sort_ord;
+val var_ord = prod_ord indexname_ord typ_ord;
+
+
+local
+
+fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
+  | hd_depth p = p;
+
+fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
+  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
+  | dest_hd (Var v) = (v, 2)
+  | dest_hd (Bound i) = ((("", i), dummyT), 3)
+  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
+
+in
+
+fun term_ord tu =
+  if pointer_eq tu then EQUAL
+  else
+    (case tu of
+      (Abs (_, T, t), Abs(_, U, u)) =>
+        (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
+    | (t, u) =>
+        (case int_ord (size_of_term t, size_of_term u) of
+          EQUAL =>
+            (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
+              EQUAL => args_ord (t, u) | ord => ord)
+        | ord => ord))
+and hd_ord (f, g) =
+  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
+and args_ord (f $ t, g $ u) =
+      (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
+  | args_ord _ = EQUAL;
+
+fun termless tu = (term_ord tu = LESS);
+
+end;
+
+
+(* Lexicographic path order on terms *)
+
+(*
+  See Baader & Nipkow, Term rewriting, CUP 1998.
+  Without variables.  Const, Var, Bound, Free and Abs are treated all as
+  constants.
+
+  f_ord maps terms to integers and serves two purposes:
+  - Predicate on constant symbols.  Those that are not recognised by f_ord
+    must be mapped to ~1.
+  - Order on the recognised symbols.  These must be mapped to distinct
+    integers >= 0.
+  The argument of f_ord is never an application.
+*)
+
+local
+
+fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
+  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
+  | unrecognized (Var v) = ((1, v), 1)
+  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
+  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
+
+fun dest_hd f_ord t =
+  let val ord = f_ord t
+  in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
+
+fun term_lpo f_ord (s, t) =
+  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
+    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
+    then case hd_ord f_ord (f, g) of
+        GREATER =>
+          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+          then GREATER else LESS
+      | EQUAL =>
+          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+          then list_ord (term_lpo f_ord) (ss, ts)
+          else LESS
+      | LESS => LESS
+    else GREATER
+  end
+and hd_ord f_ord (f, g) = case (f, g) of
+    (Abs (_, T, t), Abs (_, U, u)) =>
+      (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
+  | (_, _) => prod_ord (prod_ord int_ord
+                  (prod_ord indexname_ord typ_ord)) int_ord
+                (dest_hd f_ord f, dest_hd f_ord g);
+
+in
+val term_lpo = term_lpo
+end;
+
+
+end;
+
+structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
+structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
+structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/term_subst.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/term_subst.ML
-    ID:         $Id$
     Author:     Makarius
 
 Efficient term substitution -- avoids copying.
@@ -163,9 +162,9 @@
 
 fun zero_var_indexes_inst ts =
   let
-    val tvars = sort Term.tvar_ord (fold Term.add_tvars ts []);
+    val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []);
     val instT = map (apsnd TVar) (zero_var_inst tvars);
-    val vars = sort Term.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
+    val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
     val inst = map (apsnd Var) (zero_var_inst vars);
   in (instT, inst) end;
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/thm.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,6 @@
 (*  Title:      Pure/thm.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
+    Author:     Makarius
 
 The very core of Isabelle's Meta Logic: certified types and terms,
 derivations, theorems, framework rules (including lifting and
@@ -380,9 +379,9 @@
 
 fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
 
-val union_hyps = OrdList.union Term.fast_term_ord;
-val insert_hyps = OrdList.insert Term.fast_term_ord;
-val remove_hyps = OrdList.remove Term.fast_term_ord;
+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;
 
 
 (* merge theories of cterms/thms -- trivial absorption only *)
@@ -1561,9 +1560,9 @@
 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
 fun could_bires (Hs, B, eres_flg, rule) =
-    let fun could_reshyp (A1::_) = exists (fn H => could_unify (A1, H)) Hs
+    let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
           | could_reshyp [] = false;  (*no premise -- illegal*)
-    in  could_unify(concl_of rule, B) andalso
+    in  Term.could_unify(concl_of rule, B) andalso
         (not eres_flg  orelse  could_reshyp (prems_of rule))
     end;
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/type.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/type.ML
-    ID:         $Id$
     Author:     Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel
 
 Type signatures and certified types, special treatment of type vars,
@@ -401,7 +400,7 @@
     fun occ (Type (_, Ts)) = exists occ Ts
       | occ (TFree _) = false
       | occ (TVar (w, S)) =
-          eq_ix (v, w) orelse
+          Term.eq_ix (v, w) orelse
             (case lookup tye (w, S) of
               NONE => false
             | SOME U => occ U);
@@ -438,7 +437,7 @@
     fun unif (ty1, ty2) tye =
       (case (devar tye ty1, devar tye ty2) of
         (T as TVar (v, S1), U as TVar (w, S2)) =>
-          if eq_ix (v, w) then
+          if Term.eq_ix (v, w) then
             if S1 = S2 then tye else tvar_clash v S1 S2
           else if Sorts.sort_le classes (S1, S2) then
             Vartab.update_new (w, (S2, T)) tye
@@ -466,7 +465,7 @@
 fun raw_unify (ty1, ty2) tye =
   (case (devar tye ty1, devar tye ty2) of
     (T as TVar (v, S1), U as TVar (w, S2)) =>
-      if eq_ix (v, w) then
+      if Term.eq_ix (v, w) then
         if S1 = S2 then tye else tvar_clash v S1 S2
       else Vartab.update_new (w, (S2, T)) tye
   | (TVar (v, S), T) =>
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/unify.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/unify.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
 
@@ -104,7 +103,7 @@
   | occur (Free _)  = false
   | occur (Var (w, T))  =
       if member (op =) (!seen) w then false
-      else if eq_ix(v,w) then true
+      else if Term.eq_ix (v, w) then true
         (*no need to lookup: v has no assignment*)
       else (seen := w:: !seen;
             case Envir.lookup (env, (w, T)) of
@@ -167,7 +166,7 @@
   | occur (Free _)  = NoOcc
   | occur (Var (w, T))  =
       if member (op =) (!seen) w then NoOcc
-      else if eq_ix(v,w) then Rigid
+      else if Term.eq_ix (v, w) then Rigid
       else (seen := w:: !seen;
             case Envir.lookup (env, (w, T)) of
           NONE    => NoOcc
@@ -176,7 +175,7 @@
   | occur (t as f$_) =  (*switch to nonrigid search?*)
      (case head_of_in (env,f) of
         Var (w,_) => (*w is not assigned*)
-    if eq_ix(v,w) then Rigid
+    if Term.eq_ix (v, w) then Rigid
     else  nonrigid t
       | Abs(_,_,body) => nonrigid t (*not in normal form*)
       | _ => occomb t)
@@ -541,10 +540,10 @@
   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   in  case  (head_of t, head_of u) of
       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
-  if eq_ix(v,w) then     (*...occur check would falsely return true!*)
+  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 Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
+  else if TermOrd.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])
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Sequents/modal.ML
--- a/src/Sequents/modal.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Sequents/modal.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,8 @@
 (*  Title:      Sequents/modal.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Simple modal reasoner
+Simple modal reasoner.
 *)
 
 
@@ -39,7 +38,7 @@
   Assumes each formula in seqc is surrounded by sequence variables
   -- checks that each concl formula looks like some subgoal formula.*)
 fun could_res (seqp,seqc) =
-      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
+      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
                               (forms_of_seq seqp))
              (forms_of_seq seqc);
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Sequents/prover.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,8 @@
-(*  Title:      Sequents/prover
-    ID:         $Id$
+(*  Title:      Sequents/prover.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Simple classical reasoner for the sequent calculus, based on "theorem packs"
+Simple classical reasoner for the sequent calculus, based on "theorem packs".
 *)
 
 
@@ -65,7 +64,7 @@
   -- checks that each concl formula looks like some subgoal formula.
   It SHOULD check order as well, using recursion rather than forall/exists*)
 fun could_res (seqp,seqc) =
-      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
+      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
                               (forms_of_seq seqp))
              (forms_of_seq seqc);
 
@@ -78,7 +77,7 @@
 	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
     | (_ $ Abs(_,_,leftp) $ rightp,
        _ $ Abs(_,_,leftc) $ rightc) =>
-	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
+	  could_res (leftp,leftc)  andalso  Term.could_unify (rightp,rightc)
     | _ => false;
 
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Tools/Compute_Oracle/compute.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/compute.ML
-    ID:         $Id$
     Author:     Steven Obua
 *)
 
@@ -168,7 +167,7 @@
   | machine_of_prog (ProgHaskell _) = HASKELL
   | machine_of_prog (ProgSML _) = SML
 
-structure Sorttab = TableFun(type key = sort val ord = Term.sort_ord)
+structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
 
 type naming = int -> string
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Tools/Compute_Oracle/linker.ML
--- a/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/linker.ML
-    ID:         $Id$
     Author:     Steven Obua
 
 Linker.ML solves the problem that the computing oracle does not
@@ -51,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) Term.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) TermOrd.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))
 
 
@@ -71,7 +70,7 @@
     handle Type.TYPE_MATCH => NONE
 
 fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
-    (list_ord (prod_ord Term.fast_indexname_ord (prod_ord Term.sort_ord Term.typ_ord))) (Vartab.dest A, Vartab.dest B)
+    (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
 
 structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
 
@@ -379,7 +378,7 @@
         ComputeThm (hyps, shyps, prop)
     end
 
-val cthm_ord' = prod_ord (prod_ord (list_ord Term.term_ord) (list_ord Term.sort_ord)) Term.term_ord
+val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord
 
 fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
 
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/ZF/arith_data.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      ZF/arith_data.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
 
 Arithmetic simplification: cancellation of common terms
 *)
@@ -106,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 Term.term_ord (dest_prod t)));
+fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
 
 (*Find first coefficient-term THAT MATCHES u*)
 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
diff -r 6aefc5ff8e63 -r 5c25a2012975 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/ZF/int_arith.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      ZF/int_arith.ML
-    ID:         $Id$
     Author:     Larry Paulson
-    Copyright   2000  University of Cambridge
 
 Simprocs for linear arithmetic.
 *)
@@ -72,7 +70,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 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 ts') end;