moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
authorwenzelm
Wed Dec 31 15:30:10 2008 +0100 (2008-12-31)
changeset 292695c25a2012975
parent 29268 6aefc5ff8e63
child 29270 0eade173f77e
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
src/CCL/Wfd.thy
src/FOLP/IFOLP.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Import/shuffler.ML
src/HOL/OrderedGroup.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/function_package/decompose.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/nat_simprocs.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/reflection.ML
src/Provers/Arith/cancel_factor.ML
src/Provers/Arith/cancel_sums.ML
src/Provers/eqsubst.ML
src/Pure/IsaMakefile
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/rule_cases.ML
src/Pure/ROOT.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.ML
src/Pure/term_ord.ML
src/Pure/term_subst.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/unify.ML
src/Sequents/modal.ML
src/Sequents/prover.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/Compute_Oracle/linker.ML
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/src/CCL/Wfd.thy	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/CCL/Wfd.thy	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -434,9 +434,9 @@
     1.4    | get_bno l n (Bound m) = (m-length(l),n)
     1.5  
     1.6  (* Not a great way of identifying induction hypothesis! *)
     1.7 -fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse
     1.8 -                 could_unify(x,hd (prems_of @{thm rcall2T})) orelse
     1.9 -                 could_unify(x,hd (prems_of @{thm rcall3T}))
    1.10 +fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse
    1.11 +                 Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse
    1.12 +                 Term.could_unify(x,hd (prems_of @{thm rcall3T}))
    1.13  
    1.14  fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
    1.15    let val bvs = bvars Bi []
     2.1 --- a/src/FOLP/IFOLP.thy	Wed Dec 31 00:08:14 2008 +0100
     2.2 +++ b/src/FOLP/IFOLP.thy	Wed Dec 31 15:30:10 2008 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      FOLP/IFOLP.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Martin D Coen, Cambridge University Computer Laboratory
     2.7      Copyright   1992  University of Cambridge
     2.8  *)
     2.9 @@ -247,7 +246,7 @@
    2.10            and concl = discard_proof (Logic.strip_assums_concl prem)
    2.11        in
    2.12            if exists (fn hyp => hyp aconv concl) hyps
    2.13 -          then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
    2.14 +          then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
    2.15                     [_] => assume_tac i
    2.16                   |  _  => no_tac
    2.17            else no_tac
     3.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Dec 31 00:08:14 2008 +0100
     3.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Dec 31 15:30:10 2008 +0100
     3.3 @@ -1,8 +1,7 @@
     3.4 -(*
     3.5 -  Title:     The algebraic hierarchy of rings as axiomatic classes
     3.6 -  Id:        $Id$
     3.7 -  Author:    Clemens Ballarin, started 9 December 1996
     3.8 -  Copyright: Clemens Ballarin
     3.9 +(*  Title:     HOL/Algebra/abstract/Ring2.thy
    3.10 +    Author:    Clemens Ballarin
    3.11 +
    3.12 +The algebraic hierarchy of rings as axiomatic classes.
    3.13  *)
    3.14  
    3.15  header {* The algebraic hierarchy of rings as type classes *}
    3.16 @@ -211,7 +210,7 @@
    3.17          @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
    3.18    | ring_ord _ = ~1;
    3.19  
    3.20 -fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    3.21 +fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
    3.22  
    3.23  val ring_ss = HOL_basic_ss settermless termless_ring addsimps
    3.24    [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
     4.1 --- a/src/HOL/Algebra/ringsimp.ML	Wed Dec 31 00:08:14 2008 +0100
     4.2 +++ b/src/HOL/Algebra/ringsimp.ML	Wed Dec 31 15:30:10 2008 +0100
     4.3 @@ -1,6 +1,4 @@
     4.4 -(*
     4.5 -  Id:        $Id$
     4.6 -  Author:    Clemens Ballarin
     4.7 +(*  Author:    Clemens Ballarin
     4.8  
     4.9  Normalisation method for locales ring and cring.
    4.10  *)
    4.11 @@ -48,7 +46,7 @@
    4.12      val ops = map (fst o Term.strip_comb) ts;
    4.13      fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
    4.14        | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
    4.15 -    fun less (a, b) = (Term.term_lpo ord (a, b) = LESS);
    4.16 +    fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
    4.17    in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
    4.18  
    4.19  fun algebra_tac ctxt =
     5.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:14 2008 +0100
     5.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
     5.3 @@ -353,7 +353,7 @@
     5.4  
     5.5  fun equals_fun thy assume t =
     5.6      case t of
     5.7 -        Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
     5.8 +        Const("op ==",_) $ u $ v => if TermOrd.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/OrderedGroup.thy	Wed Dec 31 00:08:14 2008 +0100
     6.2 +++ b/src/HOL/OrderedGroup.thy	Wed Dec 31 15:30:10 2008 +0100
     6.3 @@ -1,7 +1,5 @@
     6.4  (*  Title:   HOL/OrderedGroup.thy
     6.5 -    ID:      $Id$
     6.6 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
     6.7 -             with contributions by Jeremy Avigad
     6.8 +    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
     6.9  *)
    6.10  
    6.11  header {* Ordered Groups *}
    6.12 @@ -1376,7 +1374,7 @@
    6.13          @{const_name HOL.uminus}, @{const_name HOL.minus}]
    6.14    | agrp_ord _ = ~1;
    6.15  
    6.16 -fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    6.17 +fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
    6.18  
    6.19  local
    6.20    val ac1 = mk_meta_eq @{thm add_assoc};
     7.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Dec 31 00:08:14 2008 +0100
     7.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Dec 31 15:30:10 2008 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4 -(*  Title:      DistinctTreeProver.thy
     7.5 -    ID:         $Id$
     7.6 +(*  Title:      HOL/Statespace/DistinctTreeProver.thy
     7.7      Author:     Norbert Schirmer, TU Muenchen
     7.8  *)
     7.9  
    7.10 @@ -646,9 +645,9 @@
    7.11  val const_decls = map (fn i => Syntax.no_syn 
    7.12                                   ("const" ^ string_of_int i,Type ("nat",[]))) nums
    7.13  
    7.14 -val consts = sort Term.fast_term_ord 
    7.15 +val consts = sort TermOrd.fast_term_ord 
    7.16                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
    7.17 -val consts' = sort Term.fast_term_ord 
    7.18 +val consts' = sort TermOrd.fast_term_ord 
    7.19                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
    7.20  
    7.21  val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
     8.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Dec 31 00:08:14 2008 +0100
     8.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Dec 31 15:30:10 2008 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4 -(*  Title:      distinct_tree_prover.thy
     8.5 -    ID:         $Id$
     8.6 +(*  Title:      HOL/Statespace/distinct_tree_prover.ML
     8.7      Author:     Norbert Schirmer, TU Muenchen
     8.8  *)
     8.9  
    8.10 @@ -83,7 +82,7 @@
    8.11    | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
    8.12  
    8.13  fun find_tree e t =
    8.14 -  (case bin_find_tree Term.fast_term_ord e t of
    8.15 +  (case bin_find_tree TermOrd.fast_term_ord e t of
    8.16       NONE => lin_find_tree e t
    8.17     | x => x);
    8.18  
     9.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Dec 31 00:08:14 2008 +0100
     9.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Dec 31 15:30:10 2008 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
     9.5 -    ID:         $Id$
     9.6      Author:     Amine Chaieb, TU Muenchen
     9.7  *)
     9.8  
     9.9 @@ -599,14 +598,14 @@
    9.10       if length ideal = 2 then ideal else [eq_commute, eq_commute]
    9.11    val ring_dest_neg =
    9.12      fn t => let val (l,r) = dest_comb t in
    9.13 -        if could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
    9.14 +        if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
    9.15        end
    9.16  
    9.17   val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
    9.18  (*
    9.19   fun ring_dest_inv t =
    9.20      let val (l,r) = dest_comb t in
    9.21 -        if could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
    9.22 +        if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
    9.23      end
    9.24  *)
    9.25   val ring_dest_add = dest_binary ring_add_tm;
    9.26 @@ -687,7 +686,7 @@
    9.27    val cjs = conjs tm
    9.28    val  rawvars = fold_rev (fn eq => fn a =>
    9.29                                         grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs []
    9.30 -  val vars = sort (fn (x, y) => Term.term_ord(term_of x,term_of y))
    9.31 +  val vars = sort (fn (x, y) => TermOrd.term_ord(term_of x,term_of y))
    9.32                    (distinct (op aconvc) rawvars)
    9.33   in (vars,map (grobify_equation vars) cjs)
    9.34   end;
    9.35 @@ -896,7 +895,7 @@
    9.36    val vars = filter (fn v => free_in v eq) evs
    9.37    val (qs,p) = isolate_monomials vars eq
    9.38    val rs = ideal (qs @ ps) p 
    9.39 -              (fn (s,t) => Term.term_ord (term_of s, term_of t))
    9.40 +              (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
    9.41   in (eq,Library.take (length qs, rs) ~~ vars)
    9.42   end;
    9.43   fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
    10.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Dec 31 00:08:14 2008 +0100
    10.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Dec 31 15:30:10 2008 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Amine Chaieb, TU Muenchen
    10.7  *)
    10.8  
    10.9 @@ -615,7 +614,7 @@
   10.10  val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
   10.11                                addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
   10.12  
   10.13 -fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS;
   10.14 +fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
   10.15  
   10.16  fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
   10.17                                       {conv, dest_const, mk_const, is_const}) ord =
    11.1 --- a/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 00:08:14 2008 +0100
    11.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 15:30:10 2008 +0100
    11.3 @@ -1,3 +1,7 @@
    11.4 +(*  Title:      HOL/Tools/Qelim/langford.ML
    11.5 +    Author:     Amine Chaieb, TU Muenchen
    11.6 +*)
    11.7 +
    11.8  signature LANGFORD_QE = 
    11.9  sig
   11.10    val dlo_tac : Proof.context -> int -> tactic
   11.11 @@ -211,7 +215,7 @@
   11.12   let 
   11.13     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   11.14     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   11.15 -   val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
   11.16 +   val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
   11.17     val p' = fold_rev gen ts p
   11.18   in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   11.19  
    12.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 00:08:14 2008 +0100
    12.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 15:30:10 2008 +0100
    12.3 @@ -103,7 +103,7 @@
    12.4   let 
    12.5     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    12.6     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    12.7 -   val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
    12.8 +   val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
    12.9     val p' = fold_rev gen ts p
   12.10   in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   12.11  
    13.1 --- a/src/HOL/Tools/function_package/decompose.ML	Wed Dec 31 00:08:14 2008 +0100
    13.2 +++ b/src/HOL/Tools/function_package/decompose.ML	Wed Dec 31 15:30:10 2008 +0100
    13.3 @@ -19,7 +19,7 @@
    13.4  structure Decompose : DECOMPOSE =
    13.5  struct
    13.6  
    13.7 -structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
    13.8 +structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
    13.9  
   13.10  
   13.11  fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
    14.1 --- a/src/HOL/Tools/function_package/termination.ML	Wed Dec 31 00:08:14 2008 +0100
    14.2 +++ b/src/HOL/Tools/function_package/termination.ML	Wed Dec 31 15:30:10 2008 +0100
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:       HOL/Tools/function_package/termination_data.ML
    14.5 +(*  Title:       HOL/Tools/function_package/termination.ML
    14.6      Author:      Alexander Krauss, TU Muenchen
    14.7  
    14.8  Context data for termination proofs
    14.9 @@ -50,9 +50,9 @@
   14.10  
   14.11  open FundefLib
   14.12  
   14.13 -val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
   14.14 +val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
   14.15  structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
   14.16 -structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
   14.17 +structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
   14.18  
   14.19  (** Analyzing binary trees **)
   14.20  
    15.1 --- a/src/HOL/Tools/int_arith.ML	Wed Dec 31 00:08:14 2008 +0100
    15.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Dec 31 15:30:10 2008 +0100
    15.3 @@ -1,5 +1,4 @@
    15.4 -(*  Title:      HOL/int_arith1.ML
    15.5 -    ID:         $Id$
    15.6 +(*  Title:      HOL/Tools/int_arith1.ML
    15.7      Authors:    Larry Paulson and Tobias Nipkow
    15.8  
    15.9  Simprocs and decision procedure for linear arithmetic.
   15.10 @@ -66,12 +65,12 @@
   15.11      EQUAL => int_ord (Int.sign i, Int.sign j) 
   15.12    | ord => ord);
   15.13  
   15.14 -(*This resembles Term.term_ord, but it puts binary numerals before other
   15.15 +(*This resembles TermOrd.term_ord, but it puts binary numerals before other
   15.16    non-atomic terms.*)
   15.17  local open Term 
   15.18  in 
   15.19  fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
   15.20 -      (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   15.21 +      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
   15.22    | numterm_ord
   15.23       (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
   15.24       num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
   15.25 @@ -81,7 +80,7 @@
   15.26        (case int_ord (size_of_term t, size_of_term u) of
   15.27          EQUAL =>
   15.28            let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   15.29 -            (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
   15.30 +            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
   15.31            end
   15.32        | ord => ord)
   15.33  and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
   15.34 @@ -164,7 +163,7 @@
   15.35  (*Express t as a product of (possibly) a numeral with other sorted terms*)
   15.36  fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   15.37    | dest_coeff sign t =
   15.38 -    let val ts = sort Term.term_ord (dest_prod t)
   15.39 +    let val ts = sort TermOrd.term_ord (dest_prod t)
   15.40          val (n, ts') = find_first_numeral [] ts
   15.41                            handle TERM _ => (1, ts)
   15.42      in (sign*n, mk_prod (Term.fastype_of t) ts') end;
    16.1 --- a/src/HOL/Tools/nat_simprocs.ML	Wed Dec 31 00:08:14 2008 +0100
    16.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Wed Dec 31 15:30:10 2008 +0100
    16.3 @@ -1,7 +1,5 @@
    16.4 -(*  Title:      HOL/nat_simprocs.ML
    16.5 -    ID:         $Id$
    16.6 +(*  Title:      HOL/Tools/nat_simprocs.ML
    16.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.8 -    Copyright   2000  University of Cambridge
    16.9  
   16.10  Simprocs for nat numerals.
   16.11  *)
   16.12 @@ -81,7 +79,7 @@
   16.13  
   16.14  (*Express t as a product of (possibly) a numeral with other factors, sorted*)
   16.15  fun dest_coeff t =
   16.16 -    let val ts = sort Term.term_ord (dest_prod t)
   16.17 +    let val ts = sort TermOrd.term_ord (dest_prod t)
   16.18          val (n, _, ts') = find_first_numeral [] ts
   16.19                            handle TERM _ => (1, one, ts)
   16.20      in (n, mk_prod ts') end;
    17.1 --- a/src/HOL/Tools/sat_funcs.ML	Wed Dec 31 00:08:14 2008 +0100
    17.2 +++ b/src/HOL/Tools/sat_funcs.ML	Wed Dec 31 15:30:10 2008 +0100
    17.3 @@ -1,9 +1,6 @@
    17.4  (*  Title:      HOL/Tools/sat_funcs.ML
    17.5 -    ID:         $Id$
    17.6      Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
    17.7 -    Author:     Tjark Weber
    17.8 -    Copyright   2005-2006
    17.9 -
   17.10 +    Author:     Tjark Weber, TU Muenchen
   17.11  
   17.12  Proof reconstruction from SAT solvers.
   17.13  
   17.14 @@ -323,7 +320,7 @@
   17.15  	(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
   17.16  	(* terms sorted in descending order, while only linear for terms      *)
   17.17  	(* sorted in ascending order                                          *)
   17.18 -	val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   17.19 +	val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   17.20  	val _ = if !trace_sat then
   17.21  			tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
   17.22  		else ()
    18.1 --- a/src/HOL/ex/reflection.ML	Wed Dec 31 00:08:14 2008 +0100
    18.2 +++ b/src/HOL/ex/reflection.ML	Wed Dec 31 15:30:10 2008 +0100
    18.3 @@ -1,19 +1,18 @@
    18.4 -(*
    18.5 -    ID:         $Id$
    18.6 -    Author:     Amine Chaieb, TU Muenchen
    18.7 +(*  Author:     Amine Chaieb, TU Muenchen
    18.8  
    18.9  A trial for automatical reification.
   18.10  *)
   18.11  
   18.12 -signature REFLECTION = sig
   18.13 +signature REFLECTION =
   18.14 +sig
   18.15    val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
   18.16    val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
   18.17    val gen_reflection_tac: Proof.context -> (cterm -> thm)
   18.18      -> thm list -> thm list -> term option -> int -> tactic
   18.19  end;
   18.20  
   18.21 -structure Reflection : REFLECTION
   18.22 -= struct
   18.23 +structure Reflection : REFLECTION =
   18.24 +struct
   18.25  
   18.26  val ext2 = thm "ext2";
   18.27  val nth_Cons_0 = thm "nth_Cons_0";
   18.28 @@ -38,7 +37,7 @@
   18.29     val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
   18.30     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
   18.31     fun add_fterms (t as t1 $ t2) = 
   18.32 -       if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
   18.33 +       if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
   18.34         else add_fterms t1 #> add_fterms t2
   18.35       | add_fterms (t as Abs(xn,xT,t')) = 
   18.36         if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
   18.37 @@ -139,7 +138,7 @@
   18.38          val (tyenv, tmenv) =
   18.39          Pattern.match thy
   18.40          ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
   18.41 -        (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
   18.42 +        (Envir.type_env (Envir.empty 0), Vartab.empty)
   18.43          val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
   18.44          val (fts,its) = 
   18.45  	    (map (snd o snd) fnvs,
   18.46 @@ -191,7 +190,7 @@
   18.47     val rhs_P = subst_free subst rhs
   18.48     val (tyenv, tmenv) = Pattern.match 
   18.49  	                    thy (rhs_P, t)
   18.50 -	                    (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
   18.51 +	                    (Envir.type_env (Envir.empty 0), Vartab.empty)
   18.52     val sbst = Envir.subst_vars (tyenv, tmenv)
   18.53     val sbsT = Envir.typ_subst_TVars tyenv
   18.54     val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) 
    19.1 --- a/src/Provers/Arith/cancel_factor.ML	Wed Dec 31 00:08:14 2008 +0100
    19.2 +++ b/src/Provers/Arith/cancel_factor.ML	Wed Dec 31 15:30:10 2008 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      Provers/Arith/cancel_factor.ML
    19.5 -    ID:         $Id$
    19.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    19.7  
    19.8  Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
    19.9 @@ -36,7 +35,7 @@
   19.10        if t aconv u then (u, k + 1) :: uks
   19.11        else (t, 1) :: (u, k) :: uks;
   19.12  
   19.13 -fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);
   19.14 +fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
   19.15  
   19.16  
   19.17  (* divide sum *)
    20.1 --- a/src/Provers/Arith/cancel_sums.ML	Wed Dec 31 00:08:14 2008 +0100
    20.2 +++ b/src/Provers/Arith/cancel_sums.ML	Wed Dec 31 15:30:10 2008 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      Provers/Arith/cancel_sums.ML
    20.5 -    ID:         $Id$
    20.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    20.7  
    20.8  Cancel common summands of balanced expressions:
    20.9 @@ -38,11 +37,11 @@
   20.10  fun cons2 y (x, ys, z) = (x, y :: ys, z);
   20.11  fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
   20.12  
   20.13 -(*symmetric difference of multisets -- assumed to be sorted wrt. Logic.term_ord*)
   20.14 +(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*)
   20.15  fun cancel ts [] vs = (ts, [], vs)
   20.16    | cancel [] us vs = ([], us, vs)
   20.17    | cancel (t :: ts) (u :: us) vs =
   20.18 -      (case Term.term_ord (t, u) of
   20.19 +      (case TermOrd.term_ord (t, u) of
   20.20          EQUAL => cancel ts us (t :: vs)
   20.21        | LESS => cons1 t (cancel ts (u :: us) vs)
   20.22        | GREATER => cons2 u (cancel (t :: ts) us vs));
   20.23 @@ -64,7 +63,7 @@
   20.24    | SOME bal =>
   20.25        let
   20.26          val thy = ProofContext.theory_of (Simplifier.the_context ss);
   20.27 -        val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
   20.28 +        val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal;
   20.29          val (ts', us', vs) = cancel ts us [];
   20.30        in
   20.31          if null vs then NONE
    21.1 --- a/src/Provers/eqsubst.ML	Wed Dec 31 00:08:14 2008 +0100
    21.2 +++ b/src/Provers/eqsubst.ML	Wed Dec 31 15:30:10 2008 +0100
    21.3 @@ -1,13 +1,12 @@
    21.4  (*  Title:      Provers/eqsubst.ML
    21.5 -    ID:         $Id$
    21.6 -    Author:     Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
    21.7 +    Author:     Lucas Dixon, University of Edinburgh
    21.8  
    21.9  A proof method to perform a substiution using an equation.
   21.10  *)
   21.11  
   21.12  signature EQSUBST =
   21.13  sig
   21.14 -  (* a type abriviation for match information *)
   21.15 +  (* a type abbreviation for match information *)
   21.16    type match =
   21.17         ((indexname * (sort * typ)) list (* type instantiations *)
   21.18          * (indexname * (typ * term)) list) (* term instantiations *)
   21.19 @@ -224,7 +223,7 @@
   21.20        (* is it OK to ignore the type instantiation info?
   21.21           or should I be using it? *)
   21.22        val typs_unify =
   21.23 -          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
   21.24 +          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
   21.25              handle Type.TUNIFY => NONE;
   21.26      in
   21.27        case typs_unify of
    22.1 --- a/src/Pure/IsaMakefile	Wed Dec 31 00:08:14 2008 +0100
    22.2 +++ b/src/Pure/IsaMakefile	Wed Dec 31 15:30:10 2008 +0100
    22.3 @@ -82,8 +82,8 @@
    22.4    logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    22.5    old_goals.ML old_term.ML pattern.ML primitive_defs.ML proofterm.ML	\
    22.6    pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML	\
    22.7 -  subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
    22.8 -  thm.ML type.ML type_infer.ML unify.ML variable.ML			\
    22.9 +  subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML	\
   22.10 +  theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML		\
   22.11    ../Tools/quickcheck.ML
   22.12  	@./mk
   22.13  
    23.1 --- a/src/Pure/Isar/find_theorems.ML	Wed Dec 31 00:08:14 2008 +0100
    23.2 +++ b/src/Pure/Isar/find_theorems.ML	Wed Dec 31 15:30:10 2008 +0100
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      Pure/Isar/find_theorems.ML
    23.5 -    ID:         $Id$
    23.6      Author:     Rafal Kolanski and Gerwin Klein, NICTA
    23.7  
    23.8  Retrieve theorems from proof context.
    23.9 @@ -287,7 +286,7 @@
   23.10  
   23.11  fun rem_thm_dups xs =
   23.12    xs ~~ (1 upto length xs)
   23.13 -  |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
   23.14 +  |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
   23.15    |> rem_cdups
   23.16    |> sort (int_ord o pairself #2)
   23.17    |> map #1;
    24.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 31 00:08:14 2008 +0100
    24.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 31 15:30:10 2008 +0100
    24.3 @@ -1,6 +1,6 @@
    24.4  (*  Title:      Pure/Isar/locale.ML
    24.5 -    ID:         $Id$
    24.6 -    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
    24.7 +    Author:     Clemens Ballarin, TU Muenchen
    24.8 +    Author:     Markus Wenzel, LMU/TU Muenchen
    24.9  
   24.10  Locales -- Isar proof contexts as meta-level predicates, with local
   24.11  syntax and implicit structures.
   24.12 @@ -1297,7 +1297,7 @@
   24.13  
   24.14  fun defs_ord (defs1, defs2) =
   24.15      list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
   24.16 -      Term.fast_term_ord (d1, d2)) (defs1, defs2);
   24.17 +      TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
   24.18  structure Defstab =
   24.19      TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
   24.20  
    25.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Dec 31 00:08:14 2008 +0100
    25.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Dec 31 15:30:10 2008 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      Pure/Isar/rule_cases.ML
    25.5 -    ID:         $Id$
    25.6      Author:     Markus Wenzel, TU Muenchen
    25.7  
    25.8  Annotations and local contexts of rules.
    25.9 @@ -319,7 +318,7 @@
   25.10  local
   25.11  
   25.12  fun equal_cterms ts us =
   25.13 -  is_equal (list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us));
   25.14 +  is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
   25.15  
   25.16  fun prep_rule n th =
   25.17    let
    26.1 --- a/src/Pure/ROOT.ML	Wed Dec 31 00:08:14 2008 +0100
    26.2 +++ b/src/Pure/ROOT.ML	Wed Dec 31 15:30:10 2008 +0100
    26.3 @@ -25,6 +25,7 @@
    26.4  (*fundamental structures*)
    26.5  use "name.ML";
    26.6  use "term.ML";
    26.7 +use "term_ord.ML";
    26.8  use "term_subst.ML";
    26.9  use "old_term.ML";
   26.10  use "logic.ML";
    27.1 --- a/src/Pure/envir.ML	Wed Dec 31 00:08:14 2008 +0100
    27.2 +++ b/src/Pure/envir.ML	Wed Dec 31 15:30:10 2008 +0100
    27.3 @@ -1,7 +1,5 @@
    27.4  (*  Title:      Pure/envir.ML
    27.5 -    ID:         $Id$
    27.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    27.7 -    Copyright   1988  University of Cambridge
    27.8  
    27.9  Environments.  The type of a term variable / sort of a type variable is
   27.10  part of its name. The lookup function must apply type substitutions,
   27.11 @@ -118,7 +116,7 @@
   27.12  fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
   27.13        Var (nT as (name', T)) =>
   27.14          if a = name' then env     (*cycle!*)
   27.15 -        else if Term.indexname_ord (a, name') = LESS then
   27.16 +        else if TermOrd.indexname_ord (a, name') = LESS then
   27.17             (case lookup (env, nT) of  (*if already assigned, chase*)
   27.18                  NONE => update ((nT, Var (a, T)), env)
   27.19                | SOME u => vupdate ((aU, u), env))
    28.1 --- a/src/Pure/facts.ML	Wed Dec 31 00:08:14 2008 +0100
    28.2 +++ b/src/Pure/facts.ML	Wed Dec 31 15:30:10 2008 +0100
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      Pure/facts.ML
    28.5 -    ID:         $Id$
    28.6      Author:     Makarius
    28.7  
    28.8  Environment of named facts, optionally indexed by proposition.
    28.9 @@ -166,7 +165,7 @@
   28.10  
   28.11  (* indexed props *)
   28.12  
   28.13 -val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
   28.14 +val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of;
   28.15  
   28.16  fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
   28.17  fun could_unify (Facts {props, ...}) = Net.unify_term props;
    29.1 --- a/src/Pure/meta_simplifier.ML	Wed Dec 31 00:08:14 2008 +0100
    29.2 +++ b/src/Pure/meta_simplifier.ML	Wed Dec 31 15:30:10 2008 +0100
    29.3 @@ -1,6 +1,5 @@
    29.4  (*  Title:      Pure/meta_simplifier.ML
    29.5 -    ID:         $Id$
    29.6 -    Author:     Tobias Nipkow and Stefan Berghofer
    29.7 +    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
    29.8  
    29.9  Meta-level Simplification.
   29.10  *)
   29.11 @@ -788,7 +787,7 @@
   29.12    mk_eq_True = K NONE,
   29.13    reorient = default_reorient};
   29.14  
   29.15 -val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
   29.16 +val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
   29.17  
   29.18  
   29.19  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
    30.1 --- a/src/Pure/more_thm.ML	Wed Dec 31 00:08:14 2008 +0100
    30.2 +++ b/src/Pure/more_thm.ML	Wed Dec 31 15:30:10 2008 +0100
    30.3 @@ -1,5 +1,4 @@
    30.4  (*  Title:      Pure/more_thm.ML
    30.5 -    ID:         $Id$
    30.6      Author:     Makarius
    30.7  
    30.8  Further operations on type ctyp/cterm/thm, outside the inference kernel.
    30.9 @@ -128,12 +127,12 @@
   30.10      val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
   30.11      val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
   30.12    in
   30.13 -    (case Term.fast_term_ord (prop1, prop2) of
   30.14 +    (case TermOrd.fast_term_ord (prop1, prop2) of
   30.15        EQUAL =>
   30.16 -        (case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of
   30.17 +        (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of
   30.18            EQUAL =>
   30.19 -            (case list_ord Term.fast_term_ord (hyps1, hyps2) of
   30.20 -              EQUAL => list_ord Term.sort_ord (shyps1, shyps2)
   30.21 +            (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of
   30.22 +              EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2)
   30.23              | ord => ord)
   30.24          | ord => ord)
   30.25      | ord => ord)
    31.1 --- a/src/Pure/old_term.ML	Wed Dec 31 00:08:14 2008 +0100
    31.2 +++ b/src/Pure/old_term.ML	Wed Dec 31 15:30:10 2008 +0100
    31.3 @@ -17,7 +17,7 @@
    31.4  
    31.5  (*Accumulates the Vars in the term, suppressing duplicates*)
    31.6  fun add_term_vars (t, vars: term list) = case t of
    31.7 -    Var   _ => OrdList.insert Term.term_ord t vars
    31.8 +    Var   _ => OrdList.insert TermOrd.term_ord t vars
    31.9    | Abs (_,_,body) => add_term_vars(body,vars)
   31.10    | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   31.11    | _ => vars;
   31.12 @@ -26,7 +26,7 @@
   31.13  
   31.14  (*Accumulates the Frees in the term, suppressing duplicates*)
   31.15  fun add_term_frees (t, frees: term list) = case t of
   31.16 -    Free   _ => OrdList.insert Term.term_ord t frees
   31.17 +    Free   _ => OrdList.insert TermOrd.term_ord t frees
   31.18    | Abs (_,_,body) => add_term_frees(body,frees)
   31.19    | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   31.20    | _ => frees;
    32.1 --- a/src/Pure/pattern.ML	Wed Dec 31 00:08:14 2008 +0100
    32.2 +++ b/src/Pure/pattern.ML	Wed Dec 31 15:30:10 2008 +0100
    32.3 @@ -1,6 +1,5 @@
    32.4  (*  Title:      Pure/pattern.ML
    32.5 -    ID:         $Id$
    32.6 -    Author:     Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer
    32.7 +    Author:     Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen
    32.8  
    32.9  Unification of Higher-Order Patterns.
   32.10  
   32.11 @@ -223,7 +222,7 @@
   32.12                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
   32.13                   in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
   32.14                   end;
   32.15 -  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
   32.16 +  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
   32.17  
   32.18  fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
   32.19    if T=U then env
    33.1 --- a/src/Pure/proofterm.ML	Wed Dec 31 00:08:14 2008 +0100
    33.2 +++ b/src/Pure/proofterm.ML	Wed Dec 31 15:30:10 2008 +0100
    33.3 @@ -188,7 +188,7 @@
    33.4  
    33.5  (* proof body *)
    33.6  
    33.7 -val oracle_ord = prod_ord fast_string_ord Term.fast_term_ord;
    33.8 +val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
    33.9  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
   33.10  
   33.11  fun make_body prf =
    34.1 --- a/src/Pure/search.ML	Wed Dec 31 00:08:14 2008 +0100
    34.2 +++ b/src/Pure/search.ML	Wed Dec 31 15:30:10 2008 +0100
    34.3 @@ -1,5 +1,4 @@
    34.4  (*  Title:      Pure/search.ML
    34.5 -    ID:         $Id$
    34.6      Author:     Lawrence C Paulson and Norbert Voelker
    34.7  
    34.8  Search tacticals.
    34.9 @@ -42,10 +41,8 @@
   34.10  (** Instantiation of heaps for best-first search **)
   34.11  
   34.12  (*total ordering on theorems, allowing duplicates to be found*)
   34.13 -structure ThmHeap =
   34.14 -  HeapFun (type elem = int * thm
   34.15 -    val ord = Library.prod_ord Library.int_ord
   34.16 -      (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
   34.17 +structure ThmHeap = HeapFun(type elem = int * thm
   34.18 +  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of));
   34.19  
   34.20  
   34.21  structure Search : SEARCH =
    35.1 --- a/src/Pure/sorts.ML	Wed Dec 31 00:08:14 2008 +0100
    35.2 +++ b/src/Pure/sorts.ML	Wed Dec 31 15:30:10 2008 +0100
    35.3 @@ -1,5 +1,4 @@
    35.4  (*  Title:      Pure/sorts.ML
    35.5 -    ID:         $Id$
    35.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    35.7  
    35.8  The order-sorted algebra of type classes.
    35.9 @@ -74,13 +73,13 @@
   35.10  
   35.11  (** ordered lists of sorts **)
   35.12  
   35.13 -val make = OrdList.make Term.sort_ord;
   35.14 -val op subset = OrdList.subset Term.sort_ord;
   35.15 -val op union = OrdList.union Term.sort_ord;
   35.16 -val subtract = OrdList.subtract Term.sort_ord;
   35.17 +val make = OrdList.make TermOrd.sort_ord;
   35.18 +val op subset = OrdList.subset TermOrd.sort_ord;
   35.19 +val op union = OrdList.union TermOrd.sort_ord;
   35.20 +val subtract = OrdList.subtract TermOrd.sort_ord;
   35.21  
   35.22 -val remove_sort = OrdList.remove Term.sort_ord;
   35.23 -val insert_sort = OrdList.insert Term.sort_ord;
   35.24 +val remove_sort = OrdList.remove TermOrd.sort_ord;
   35.25 +val insert_sort = OrdList.insert TermOrd.sort_ord;
   35.26  
   35.27  fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   35.28    | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
    36.1 --- a/src/Pure/term.ML	Wed Dec 31 00:08:14 2008 +0100
    36.2 +++ b/src/Pure/term.ML	Wed Dec 31 15:30:10 2008 +0100
    36.3 @@ -76,9 +76,6 @@
    36.4    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    36.5    val add_term_names: term * string list -> string list
    36.6    val aconv: term * term -> bool
    36.7 -  structure Vartab: TABLE
    36.8 -  structure Typtab: TABLE
    36.9 -  structure Termtab: TABLE
   36.10    val propT: typ
   36.11    val strip_all_body: term -> term
   36.12    val strip_all_vars: term -> (string * typ) list
   36.13 @@ -92,8 +89,6 @@
   36.14    val subst_bound: term * term -> term
   36.15    val betapply: term * term -> term
   36.16    val betapplys: term * term list -> term
   36.17 -  val eq_ix: indexname * indexname -> bool
   36.18 -  val could_unify: term * term -> bool
   36.19    val subst_free: (term * term) list -> term -> term
   36.20    val abstract_over: term * term -> term
   36.21    val lambda: term -> term -> term
   36.22 @@ -156,23 +151,14 @@
   36.23    val add_free_names: term -> string list -> string list
   36.24    val add_frees: term -> (string * typ) list -> (string * typ) list
   36.25    val hidden_polymorphism: term -> (indexname * sort) list
   36.26 +  val eq_ix: indexname * indexname -> bool
   36.27 +  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   36.28 +  val eq_var: (indexname * typ) * (indexname * typ) -> bool
   36.29 +  val could_unify: term * term -> bool
   36.30    val strip_abs_eta: int -> term -> (string * typ) list * term
   36.31 -  val fast_indexname_ord: indexname * indexname -> order
   36.32 -  val indexname_ord: indexname * indexname -> order
   36.33 -  val sort_ord: sort * sort -> order
   36.34 -  val typ_ord: typ * typ -> order
   36.35 -  val fast_term_ord: term * term -> order
   36.36 -  val term_ord: term * term -> order
   36.37 -  val hd_ord: term * term -> order
   36.38 -  val termless: term * term -> bool
   36.39 -  val term_lpo: (term -> int) -> term * term -> order
   36.40    val match_bvars: (term * term) * (string * string) list -> (string * string) list
   36.41    val map_abs_vars: (string -> string) -> term -> term
   36.42    val rename_abs: term -> term -> term -> term option
   36.43 -  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   36.44 -  val eq_var: (indexname * typ) * (indexname * typ) -> bool
   36.45 -  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   36.46 -  val var_ord: (indexname * typ) * (indexname * typ) -> order
   36.47    val close_schematic_term: term -> term
   36.48    val maxidx_typ: typ -> int -> int
   36.49    val maxidx_typs: typ list -> int -> int
   36.50 @@ -514,9 +500,17 @@
   36.51  
   36.52  
   36.53  
   36.54 -(** Comparing terms, types, sorts etc. **)
   36.55 +(** Comparing terms **)
   36.56 +
   36.57 +(* variables *)
   36.58 +
   36.59 +fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   36.60  
   36.61 -(* alpha equivalence -- tuned for equalities *)
   36.62 +fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   36.63 +fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   36.64 +
   36.65 +
   36.66 +(* alpha equivalence *)
   36.67  
   36.68  fun tm1 aconv tm2 =
   36.69    pointer_eq (tm1, tm2) orelse
   36.70 @@ -526,184 +520,24 @@
   36.71      | (a1, a2) => a1 = a2);
   36.72  
   36.73  
   36.74 -(* fast syntactic ordering -- tuned for inequalities *)
   36.75 -
   36.76 -fun fast_indexname_ord ((x, i), (y, j)) =
   36.77 -  (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
   36.78 -
   36.79 -fun sort_ord SS =
   36.80 -  if pointer_eq SS then EQUAL
   36.81 -  else dict_ord fast_string_ord SS;
   36.82 -
   36.83 -local
   36.84 -
   36.85 -fun cons_nr (TVar _) = 0
   36.86 -  | cons_nr (TFree _) = 1
   36.87 -  | cons_nr (Type _) = 2;
   36.88 -
   36.89 -in
   36.90 -
   36.91 -fun typ_ord TU =
   36.92 -  if pointer_eq TU then EQUAL
   36.93 -  else
   36.94 -    (case TU of
   36.95 -      (Type (a, Ts), Type (b, Us)) =>
   36.96 -        (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
   36.97 -    | (TFree (a, S), TFree (b, S')) =>
   36.98 -        (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
   36.99 -    | (TVar (xi, S), TVar (yj, S')) =>
  36.100 -        (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
  36.101 -    | (T, U) => int_ord (cons_nr T, cons_nr U));
  36.102 -
  36.103 -end;
  36.104 -
  36.105 -local
  36.106 -
  36.107 -fun cons_nr (Const _) = 0
  36.108 -  | cons_nr (Free _) = 1
  36.109 -  | cons_nr (Var _) = 2
  36.110 -  | cons_nr (Bound _) = 3
  36.111 -  | cons_nr (Abs _) = 4
  36.112 -  | cons_nr (_ $ _) = 5;
  36.113 -
  36.114 -fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
  36.115 -  | struct_ord (t1 $ t2, u1 $ u2) =
  36.116 -      (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
  36.117 -  | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
  36.118 -
  36.119 -fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
  36.120 -  | atoms_ord (t1 $ t2, u1 $ u2) =
  36.121 -      (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
  36.122 -  | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
  36.123 -  | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
  36.124 -  | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
  36.125 -  | atoms_ord (Bound i, Bound j) = int_ord (i, j)
  36.126 -  | atoms_ord _ = sys_error "atoms_ord";
  36.127 -
  36.128 -fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
  36.129 -      (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
  36.130 -  | types_ord (t1 $ t2, u1 $ u2) =
  36.131 -      (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
  36.132 -  | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
  36.133 -  | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
  36.134 -  | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
  36.135 -  | types_ord (Bound _, Bound _) = EQUAL
  36.136 -  | types_ord _ = sys_error "types_ord";
  36.137 -
  36.138 -in
  36.139 -
  36.140 -fun fast_term_ord tu =
  36.141 -  if pointer_eq tu then EQUAL
  36.142 -  else
  36.143 -    (case struct_ord tu of
  36.144 -      EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
  36.145 -    | ord => ord);
  36.146 -
  36.147 -structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
  36.148 -structure Typtab = TableFun(type key = typ val ord = typ_ord);
  36.149 -structure Termtab = TableFun(type key = term val ord = fast_term_ord);
  36.150 -
  36.151 -end;
  36.152 -
  36.153 -
  36.154 -(* term_ord *)
  36.155 -
  36.156 -(*a linear well-founded AC-compatible ordering for terms:
  36.157 -  s < t <=> 1. size(s) < size(t) or
  36.158 -            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
  36.159 -            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
  36.160 -               (s1..sn) < (t1..tn) (lexicographically)*)
  36.161 +(*A fast unification filter: true unless the two terms cannot be unified.
  36.162 +  Terms must be NORMAL.  Treats all Vars as distinct. *)
  36.163 +fun could_unify (t, u) =
  36.164 +  let
  36.165 +    fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
  36.166 +      | matchrands _ _ = true;
  36.167 +  in
  36.168 +    case (head_of t, head_of u) of
  36.169 +      (_, Var _) => true
  36.170 +    | (Var _, _) => true
  36.171 +    | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
  36.172 +    | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
  36.173 +    | (Bound i, Bound j) => i = j andalso matchrands t u
  36.174 +    | (Abs _, _) => true   (*because of possible eta equality*)
  36.175 +    | (_, Abs _) => true
  36.176 +    | _ => false
  36.177 +  end;
  36.178  
  36.179 -fun indexname_ord ((x, i), (y, j)) =
  36.180 -  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
  36.181 -
  36.182 -local
  36.183 -
  36.184 -fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
  36.185 -  | hd_depth p = p;
  36.186 -
  36.187 -fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
  36.188 -  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
  36.189 -  | dest_hd (Var v) = (v, 2)
  36.190 -  | dest_hd (Bound i) = ((("", i), dummyT), 3)
  36.191 -  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
  36.192 -
  36.193 -in
  36.194 -
  36.195 -fun term_ord tu =
  36.196 -  if pointer_eq tu then EQUAL
  36.197 -  else
  36.198 -    (case tu of
  36.199 -      (Abs (_, T, t), Abs(_, U, u)) =>
  36.200 -        (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
  36.201 -    | (t, u) =>
  36.202 -        (case int_ord (size_of_term t, size_of_term u) of
  36.203 -          EQUAL =>
  36.204 -            (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
  36.205 -              EQUAL => args_ord (t, u) | ord => ord)
  36.206 -        | ord => ord))
  36.207 -and hd_ord (f, g) =
  36.208 -  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
  36.209 -and args_ord (f $ t, g $ u) =
  36.210 -      (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
  36.211 -  | args_ord _ = EQUAL;
  36.212 -
  36.213 -fun termless tu = (term_ord tu = LESS);
  36.214 -
  36.215 -end;
  36.216 -
  36.217 -
  36.218 -(** Lexicographic path order on terms **)
  36.219 -
  36.220 -(*
  36.221 -  See Baader & Nipkow, Term rewriting, CUP 1998.
  36.222 -  Without variables.  Const, Var, Bound, Free and Abs are treated all as
  36.223 -  constants.
  36.224 -
  36.225 -  f_ord maps terms to integers and serves two purposes:
  36.226 -  - Predicate on constant symbols.  Those that are not recognised by f_ord
  36.227 -    must be mapped to ~1.
  36.228 -  - Order on the recognised symbols.  These must be mapped to distinct
  36.229 -    integers >= 0.
  36.230 -  The argument of f_ord is never an application.
  36.231 -*)
  36.232 -
  36.233 -local
  36.234 -
  36.235 -fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
  36.236 -  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
  36.237 -  | unrecognized (Var v) = ((1, v), 1)
  36.238 -  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
  36.239 -  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
  36.240 -
  36.241 -fun dest_hd f_ord t =
  36.242 -  let val ord = f_ord t
  36.243 -  in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
  36.244 -
  36.245 -fun term_lpo f_ord (s, t) =
  36.246 -  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
  36.247 -    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
  36.248 -    then case hd_ord f_ord (f, g) of
  36.249 -        GREATER =>
  36.250 -          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
  36.251 -          then GREATER else LESS
  36.252 -      | EQUAL =>
  36.253 -          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
  36.254 -          then list_ord (term_lpo f_ord) (ss, ts)
  36.255 -          else LESS
  36.256 -      | LESS => LESS
  36.257 -    else GREATER
  36.258 -  end
  36.259 -and hd_ord f_ord (f, g) = case (f, g) of
  36.260 -    (Abs (_, T, t), Abs (_, U, u)) =>
  36.261 -      (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
  36.262 -  | (_, _) => prod_ord (prod_ord int_ord
  36.263 -                  (prod_ord indexname_ord typ_ord)) int_ord
  36.264 -                (dest_hd f_ord f, dest_hd f_ord g);
  36.265 -
  36.266 -in
  36.267 -val term_lpo = term_lpo
  36.268 -end;
  36.269  
  36.270  
  36.271  (** Connectives of higher order logic **)
  36.272 @@ -854,35 +688,6 @@
  36.273    in (vs1 @ vs2, t'') end;
  36.274  
  36.275  
  36.276 -(* comparing variables *)
  36.277 -
  36.278 -fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
  36.279 -
  36.280 -fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
  36.281 -fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
  36.282 -
  36.283 -val tvar_ord = prod_ord indexname_ord sort_ord;
  36.284 -val var_ord = prod_ord indexname_ord typ_ord;
  36.285 -
  36.286 -
  36.287 -(*A fast unification filter: true unless the two terms cannot be unified.
  36.288 -  Terms must be NORMAL.  Treats all Vars as distinct. *)
  36.289 -fun could_unify (t, u) =
  36.290 -  let
  36.291 -    fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
  36.292 -      | matchrands _ _ = true;
  36.293 -  in
  36.294 -    case (head_of t, head_of u) of
  36.295 -      (_, Var _) => true
  36.296 -    | (Var _, _) => true
  36.297 -    | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
  36.298 -    | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
  36.299 -    | (Bound i, Bound j) => i = j andalso matchrands t u
  36.300 -    | (Abs _, _) => true   (*because of possible eta equality*)
  36.301 -    | (_, Abs _) => true
  36.302 -    | _ => false
  36.303 -  end;
  36.304 -
  36.305  (*Substitute new for free occurrences of old in a term*)
  36.306  fun subst_free [] = I
  36.307    | subst_free pairs =
    37.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.2 +++ b/src/Pure/term_ord.ML	Wed Dec 31 15:30:10 2008 +0100
    37.3 @@ -0,0 +1,209 @@
    37.4 +(*  Title:      Pure/term_ord.ML
    37.5 +    Author:     Tobias Nipkow and Makarius, TU Muenchen
    37.6 +
    37.7 +Term orderings.
    37.8 +*)
    37.9 +
   37.10 +signature TERM_ORD =
   37.11 +sig
   37.12 +  val fast_indexname_ord: indexname * indexname -> order
   37.13 +  val sort_ord: sort * sort -> order
   37.14 +  val typ_ord: typ * typ -> order
   37.15 +  val fast_term_ord: term * term -> order
   37.16 +  val indexname_ord: indexname * indexname -> order
   37.17 +  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   37.18 +  val var_ord: (indexname * typ) * (indexname * typ) -> order
   37.19 +  val term_ord: term * term -> order
   37.20 +  val hd_ord: term * term -> order
   37.21 +  val termless: term * term -> bool
   37.22 +  val term_lpo: (term -> int) -> term * term -> order
   37.23 +end;
   37.24 +
   37.25 +structure TermOrd: TERM_ORD =
   37.26 +struct
   37.27 +
   37.28 +(* fast syntactic ordering -- tuned for inequalities *)
   37.29 +
   37.30 +fun fast_indexname_ord ((x, i), (y, j)) =
   37.31 +  (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
   37.32 +
   37.33 +fun sort_ord SS =
   37.34 +  if pointer_eq SS then EQUAL
   37.35 +  else dict_ord fast_string_ord SS;
   37.36 +
   37.37 +local
   37.38 +
   37.39 +fun cons_nr (TVar _) = 0
   37.40 +  | cons_nr (TFree _) = 1
   37.41 +  | cons_nr (Type _) = 2;
   37.42 +
   37.43 +in
   37.44 +
   37.45 +fun typ_ord TU =
   37.46 +  if pointer_eq TU then EQUAL
   37.47 +  else
   37.48 +    (case TU of
   37.49 +      (Type (a, Ts), Type (b, Us)) =>
   37.50 +        (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
   37.51 +    | (TFree (a, S), TFree (b, S')) =>
   37.52 +        (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
   37.53 +    | (TVar (xi, S), TVar (yj, S')) =>
   37.54 +        (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
   37.55 +    | (T, U) => int_ord (cons_nr T, cons_nr U));
   37.56 +
   37.57 +end;
   37.58 +
   37.59 +local
   37.60 +
   37.61 +fun cons_nr (Const _) = 0
   37.62 +  | cons_nr (Free _) = 1
   37.63 +  | cons_nr (Var _) = 2
   37.64 +  | cons_nr (Bound _) = 3
   37.65 +  | cons_nr (Abs _) = 4
   37.66 +  | cons_nr (_ $ _) = 5;
   37.67 +
   37.68 +fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
   37.69 +  | struct_ord (t1 $ t2, u1 $ u2) =
   37.70 +      (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
   37.71 +  | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
   37.72 +
   37.73 +fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
   37.74 +  | atoms_ord (t1 $ t2, u1 $ u2) =
   37.75 +      (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
   37.76 +  | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
   37.77 +  | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   37.78 +  | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   37.79 +  | atoms_ord (Bound i, Bound j) = int_ord (i, j)
   37.80 +  | atoms_ord _ = sys_error "atoms_ord";
   37.81 +
   37.82 +fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
   37.83 +      (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
   37.84 +  | types_ord (t1 $ t2, u1 $ u2) =
   37.85 +      (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
   37.86 +  | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
   37.87 +  | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   37.88 +  | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   37.89 +  | types_ord (Bound _, Bound _) = EQUAL
   37.90 +  | types_ord _ = sys_error "types_ord";
   37.91 +
   37.92 +in
   37.93 +
   37.94 +fun fast_term_ord tu =
   37.95 +  if pointer_eq tu then EQUAL
   37.96 +  else
   37.97 +    (case struct_ord tu of
   37.98 +      EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
   37.99 +    | ord => ord);
  37.100 +
  37.101 +end;
  37.102 +
  37.103 +
  37.104 +(* term_ord *)
  37.105 +
  37.106 +(*a linear well-founded AC-compatible ordering for terms:
  37.107 +  s < t <=> 1. size(s) < size(t) or
  37.108 +            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
  37.109 +            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
  37.110 +               (s1..sn) < (t1..tn) (lexicographically)*)
  37.111 +
  37.112 +fun indexname_ord ((x, i), (y, j)) =
  37.113 +  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
  37.114 +
  37.115 +val tvar_ord = prod_ord indexname_ord sort_ord;
  37.116 +val var_ord = prod_ord indexname_ord typ_ord;
  37.117 +
  37.118 +
  37.119 +local
  37.120 +
  37.121 +fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
  37.122 +  | hd_depth p = p;
  37.123 +
  37.124 +fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
  37.125 +  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
  37.126 +  | dest_hd (Var v) = (v, 2)
  37.127 +  | dest_hd (Bound i) = ((("", i), dummyT), 3)
  37.128 +  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
  37.129 +
  37.130 +in
  37.131 +
  37.132 +fun term_ord tu =
  37.133 +  if pointer_eq tu then EQUAL
  37.134 +  else
  37.135 +    (case tu of
  37.136 +      (Abs (_, T, t), Abs(_, U, u)) =>
  37.137 +        (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
  37.138 +    | (t, u) =>
  37.139 +        (case int_ord (size_of_term t, size_of_term u) of
  37.140 +          EQUAL =>
  37.141 +            (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
  37.142 +              EQUAL => args_ord (t, u) | ord => ord)
  37.143 +        | ord => ord))
  37.144 +and hd_ord (f, g) =
  37.145 +  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
  37.146 +and args_ord (f $ t, g $ u) =
  37.147 +      (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
  37.148 +  | args_ord _ = EQUAL;
  37.149 +
  37.150 +fun termless tu = (term_ord tu = LESS);
  37.151 +
  37.152 +end;
  37.153 +
  37.154 +
  37.155 +(* Lexicographic path order on terms *)
  37.156 +
  37.157 +(*
  37.158 +  See Baader & Nipkow, Term rewriting, CUP 1998.
  37.159 +  Without variables.  Const, Var, Bound, Free and Abs are treated all as
  37.160 +  constants.
  37.161 +
  37.162 +  f_ord maps terms to integers and serves two purposes:
  37.163 +  - Predicate on constant symbols.  Those that are not recognised by f_ord
  37.164 +    must be mapped to ~1.
  37.165 +  - Order on the recognised symbols.  These must be mapped to distinct
  37.166 +    integers >= 0.
  37.167 +  The argument of f_ord is never an application.
  37.168 +*)
  37.169 +
  37.170 +local
  37.171 +
  37.172 +fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
  37.173 +  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
  37.174 +  | unrecognized (Var v) = ((1, v), 1)
  37.175 +  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
  37.176 +  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
  37.177 +
  37.178 +fun dest_hd f_ord t =
  37.179 +  let val ord = f_ord t
  37.180 +  in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
  37.181 +
  37.182 +fun term_lpo f_ord (s, t) =
  37.183 +  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
  37.184 +    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
  37.185 +    then case hd_ord f_ord (f, g) of
  37.186 +        GREATER =>
  37.187 +          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
  37.188 +          then GREATER else LESS
  37.189 +      | EQUAL =>
  37.190 +          if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
  37.191 +          then list_ord (term_lpo f_ord) (ss, ts)
  37.192 +          else LESS
  37.193 +      | LESS => LESS
  37.194 +    else GREATER
  37.195 +  end
  37.196 +and hd_ord f_ord (f, g) = case (f, g) of
  37.197 +    (Abs (_, T, t), Abs (_, U, u)) =>
  37.198 +      (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
  37.199 +  | (_, _) => prod_ord (prod_ord int_ord
  37.200 +                  (prod_ord indexname_ord typ_ord)) int_ord
  37.201 +                (dest_hd f_ord f, dest_hd f_ord g);
  37.202 +
  37.203 +in
  37.204 +val term_lpo = term_lpo
  37.205 +end;
  37.206 +
  37.207 +
  37.208 +end;
  37.209 +
  37.210 +structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
  37.211 +structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
  37.212 +structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
    38.1 --- a/src/Pure/term_subst.ML	Wed Dec 31 00:08:14 2008 +0100
    38.2 +++ b/src/Pure/term_subst.ML	Wed Dec 31 15:30:10 2008 +0100
    38.3 @@ -1,5 +1,4 @@
    38.4  (*  Title:      Pure/term_subst.ML
    38.5 -    ID:         $Id$
    38.6      Author:     Makarius
    38.7  
    38.8  Efficient term substitution -- avoids copying.
    38.9 @@ -163,9 +162,9 @@
   38.10  
   38.11  fun zero_var_indexes_inst ts =
   38.12    let
   38.13 -    val tvars = sort Term.tvar_ord (fold Term.add_tvars ts []);
   38.14 +    val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []);
   38.15      val instT = map (apsnd TVar) (zero_var_inst tvars);
   38.16 -    val vars = sort Term.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
   38.17 +    val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
   38.18      val inst = map (apsnd Var) (zero_var_inst vars);
   38.19    in (instT, inst) end;
   38.20  
    39.1 --- a/src/Pure/thm.ML	Wed Dec 31 00:08:14 2008 +0100
    39.2 +++ b/src/Pure/thm.ML	Wed Dec 31 15:30:10 2008 +0100
    39.3 @@ -1,7 +1,6 @@
    39.4  (*  Title:      Pure/thm.ML
    39.5 -    ID:         $Id$
    39.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    39.7 -    Copyright   1994  University of Cambridge
    39.8 +    Author:     Makarius
    39.9  
   39.10  The very core of Isabelle's Meta Logic: certified types and terms,
   39.11  derivations, theorems, framework rules (including lifting and
   39.12 @@ -380,9 +379,9 @@
   39.13  
   39.14  fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
   39.15  
   39.16 -val union_hyps = OrdList.union Term.fast_term_ord;
   39.17 -val insert_hyps = OrdList.insert Term.fast_term_ord;
   39.18 -val remove_hyps = OrdList.remove Term.fast_term_ord;
   39.19 +val union_hyps = OrdList.union TermOrd.fast_term_ord;
   39.20 +val insert_hyps = OrdList.insert TermOrd.fast_term_ord;
   39.21 +val remove_hyps = OrdList.remove TermOrd.fast_term_ord;
   39.22  
   39.23  
   39.24  (* merge theories of cterms/thms -- trivial absorption only *)
   39.25 @@ -1561,9 +1560,9 @@
   39.26  (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   39.27    and conclusion B.  If eres_flg then checks 1st premise of rule also*)
   39.28  fun could_bires (Hs, B, eres_flg, rule) =
   39.29 -    let fun could_reshyp (A1::_) = exists (fn H => could_unify (A1, H)) Hs
   39.30 +    let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
   39.31            | could_reshyp [] = false;  (*no premise -- illegal*)
   39.32 -    in  could_unify(concl_of rule, B) andalso
   39.33 +    in  Term.could_unify(concl_of rule, B) andalso
   39.34          (not eres_flg  orelse  could_reshyp (prems_of rule))
   39.35      end;
   39.36  
    40.1 --- a/src/Pure/type.ML	Wed Dec 31 00:08:14 2008 +0100
    40.2 +++ b/src/Pure/type.ML	Wed Dec 31 15:30:10 2008 +0100
    40.3 @@ -1,5 +1,4 @@
    40.4  (*  Title:      Pure/type.ML
    40.5 -    ID:         $Id$
    40.6      Author:     Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel
    40.7  
    40.8  Type signatures and certified types, special treatment of type vars,
    40.9 @@ -401,7 +400,7 @@
   40.10      fun occ (Type (_, Ts)) = exists occ Ts
   40.11        | occ (TFree _) = false
   40.12        | occ (TVar (w, S)) =
   40.13 -          eq_ix (v, w) orelse
   40.14 +          Term.eq_ix (v, w) orelse
   40.15              (case lookup tye (w, S) of
   40.16                NONE => false
   40.17              | SOME U => occ U);
   40.18 @@ -438,7 +437,7 @@
   40.19      fun unif (ty1, ty2) tye =
   40.20        (case (devar tye ty1, devar tye ty2) of
   40.21          (T as TVar (v, S1), U as TVar (w, S2)) =>
   40.22 -          if eq_ix (v, w) then
   40.23 +          if Term.eq_ix (v, w) then
   40.24              if S1 = S2 then tye else tvar_clash v S1 S2
   40.25            else if Sorts.sort_le classes (S1, S2) then
   40.26              Vartab.update_new (w, (S2, T)) tye
   40.27 @@ -466,7 +465,7 @@
   40.28  fun raw_unify (ty1, ty2) tye =
   40.29    (case (devar tye ty1, devar tye ty2) of
   40.30      (T as TVar (v, S1), U as TVar (w, S2)) =>
   40.31 -      if eq_ix (v, w) then
   40.32 +      if Term.eq_ix (v, w) then
   40.33          if S1 = S2 then tye else tvar_clash v S1 S2
   40.34        else Vartab.update_new (w, (S2, T)) tye
   40.35    | (TVar (v, S), T) =>
    41.1 --- a/src/Pure/unify.ML	Wed Dec 31 00:08:14 2008 +0100
    41.2 +++ b/src/Pure/unify.ML	Wed Dec 31 15:30:10 2008 +0100
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title:      Pure/unify.ML
    41.5 -    ID:         $Id$
    41.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    41.7      Copyright   Cambridge University 1992
    41.8  
    41.9 @@ -104,7 +103,7 @@
   41.10    | occur (Free _)  = false
   41.11    | occur (Var (w, T))  =
   41.12        if member (op =) (!seen) w then false
   41.13 -      else if eq_ix(v,w) then true
   41.14 +      else if Term.eq_ix (v, w) then true
   41.15          (*no need to lookup: v has no assignment*)
   41.16        else (seen := w:: !seen;
   41.17              case Envir.lookup (env, (w, T)) of
   41.18 @@ -167,7 +166,7 @@
   41.19    | occur (Free _)  = NoOcc
   41.20    | occur (Var (w, T))  =
   41.21        if member (op =) (!seen) w then NoOcc
   41.22 -      else if eq_ix(v,w) then Rigid
   41.23 +      else if Term.eq_ix (v, w) then Rigid
   41.24        else (seen := w:: !seen;
   41.25              case Envir.lookup (env, (w, T)) of
   41.26            NONE    => NoOcc
   41.27 @@ -176,7 +175,7 @@
   41.28    | occur (t as f$_) =  (*switch to nonrigid search?*)
   41.29       (case head_of_in (env,f) of
   41.30          Var (w,_) => (*w is not assigned*)
   41.31 -    if eq_ix(v,w) then Rigid
   41.32 +    if Term.eq_ix (v, w) then Rigid
   41.33      else  nonrigid t
   41.34        | Abs(_,_,body) => nonrigid t (*not in normal form*)
   41.35        | _ => occomb t)
   41.36 @@ -541,10 +540,10 @@
   41.37    let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   41.38    in  case  (head_of t, head_of u) of
   41.39        (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   41.40 -  if eq_ix(v,w) then     (*...occur check would falsely return true!*)
   41.41 +  if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
   41.42        if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   41.43        else raise TERM ("add_ffpair: Var name confusion", [t,u])
   41.44 -  else if Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
   41.45 +  else if TermOrd.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
   41.46         clean_ffpair thy ((rbinder, u, t), (env,tpairs))
   41.47          else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
   41.48      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
    42.1 --- a/src/Sequents/modal.ML	Wed Dec 31 00:08:14 2008 +0100
    42.2 +++ b/src/Sequents/modal.ML	Wed Dec 31 15:30:10 2008 +0100
    42.3 @@ -1,9 +1,8 @@
    42.4  (*  Title:      Sequents/modal.ML
    42.5 -    ID:         $Id$
    42.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    42.7      Copyright   1992  University of Cambridge
    42.8  
    42.9 -Simple modal reasoner
   42.10 +Simple modal reasoner.
   42.11  *)
   42.12  
   42.13  
   42.14 @@ -39,7 +38,7 @@
   42.15    Assumes each formula in seqc is surrounded by sequence variables
   42.16    -- checks that each concl formula looks like some subgoal formula.*)
   42.17  fun could_res (seqp,seqc) =
   42.18 -      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
   42.19 +      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
   42.20                                (forms_of_seq seqp))
   42.21               (forms_of_seq seqc);
   42.22  
    43.1 --- a/src/Sequents/prover.ML	Wed Dec 31 00:08:14 2008 +0100
    43.2 +++ b/src/Sequents/prover.ML	Wed Dec 31 15:30:10 2008 +0100
    43.3 @@ -1,9 +1,8 @@
    43.4 -(*  Title:      Sequents/prover
    43.5 -    ID:         $Id$
    43.6 +(*  Title:      Sequents/prover.ML
    43.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.8      Copyright   1992  University of Cambridge
    43.9  
   43.10 -Simple classical reasoner for the sequent calculus, based on "theorem packs"
   43.11 +Simple classical reasoner for the sequent calculus, based on "theorem packs".
   43.12  *)
   43.13  
   43.14  
   43.15 @@ -65,7 +64,7 @@
   43.16    -- checks that each concl formula looks like some subgoal formula.
   43.17    It SHOULD check order as well, using recursion rather than forall/exists*)
   43.18  fun could_res (seqp,seqc) =
   43.19 -      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
   43.20 +      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
   43.21                                (forms_of_seq seqp))
   43.22               (forms_of_seq seqc);
   43.23  
   43.24 @@ -78,7 +77,7 @@
   43.25  	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
   43.26      | (_ $ Abs(_,_,leftp) $ rightp,
   43.27         _ $ Abs(_,_,leftc) $ rightc) =>
   43.28 -	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
   43.29 +	  could_res (leftp,leftc)  andalso  Term.could_unify (rightp,rightc)
   43.30      | _ => false;
   43.31  
   43.32  
    44.1 --- a/src/Tools/Compute_Oracle/compute.ML	Wed Dec 31 00:08:14 2008 +0100
    44.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Wed Dec 31 15:30:10 2008 +0100
    44.3 @@ -1,5 +1,4 @@
    44.4  (*  Title:      Tools/Compute_Oracle/compute.ML
    44.5 -    ID:         $Id$
    44.6      Author:     Steven Obua
    44.7  *)
    44.8  
    44.9 @@ -168,7 +167,7 @@
   44.10    | machine_of_prog (ProgHaskell _) = HASKELL
   44.11    | machine_of_prog (ProgSML _) = SML
   44.12  
   44.13 -structure Sorttab = TableFun(type key = sort val ord = Term.sort_ord)
   44.14 +structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
   44.15  
   44.16  type naming = int -> string
   44.17  
    45.1 --- a/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 00:08:14 2008 +0100
    45.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 15:30:10 2008 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      Tools/Compute_Oracle/linker.ML
    45.5 -    ID:         $Id$
    45.6      Author:     Steven Obua
    45.7  
    45.8  Linker.ML solves the problem that the computing oracle does not
    45.9 @@ -51,7 +50,7 @@
   45.10    | constant_of _ = raise Link "constant_of"
   45.11  
   45.12  fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
   45.13 -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))
   45.14 +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))
   45.15  fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
   45.16  
   45.17  
   45.18 @@ -71,7 +70,7 @@
   45.19      handle Type.TYPE_MATCH => NONE
   45.20  
   45.21  fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
   45.22 -    (list_ord (prod_ord Term.fast_indexname_ord (prod_ord Term.sort_ord Term.typ_ord))) (Vartab.dest A, Vartab.dest B)
   45.23 +    (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
   45.24  
   45.25  structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
   45.26  
   45.27 @@ -379,7 +378,7 @@
   45.28          ComputeThm (hyps, shyps, prop)
   45.29      end
   45.30  
   45.31 -val cthm_ord' = prod_ord (prod_ord (list_ord Term.term_ord) (list_ord Term.sort_ord)) Term.term_ord
   45.32 +val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord
   45.33  
   45.34  fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
   45.35  
    46.1 --- a/src/ZF/arith_data.ML	Wed Dec 31 00:08:14 2008 +0100
    46.2 +++ b/src/ZF/arith_data.ML	Wed Dec 31 15:30:10 2008 +0100
    46.3 @@ -1,7 +1,5 @@
    46.4  (*  Title:      ZF/arith_data.ML
    46.5 -    ID:         $Id$
    46.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    46.7 -    Copyright   2000  University of Cambridge
    46.8  
    46.9  Arithmetic simplification: cancellation of common terms
   46.10  *)
   46.11 @@ -106,7 +104,7 @@
   46.12  
   46.13  (*Dummy version: the "coefficient" is always 1.
   46.14    In the result, the factors are sorted terms*)
   46.15 -fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
   46.16 +fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
   46.17  
   46.18  (*Find first coefficient-term THAT MATCHES u*)
   46.19  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    47.1 --- a/src/ZF/int_arith.ML	Wed Dec 31 00:08:14 2008 +0100
    47.2 +++ b/src/ZF/int_arith.ML	Wed Dec 31 15:30:10 2008 +0100
    47.3 @@ -1,7 +1,5 @@
    47.4  (*  Title:      ZF/int_arith.ML
    47.5 -    ID:         $Id$
    47.6      Author:     Larry Paulson
    47.7 -    Copyright   2000  University of Cambridge
    47.8  
    47.9  Simprocs for linear arithmetic.
   47.10  *)
   47.11 @@ -72,7 +70,7 @@
   47.12  (*Express t as a product of (possibly) a numeral with other sorted terms*)
   47.13  fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
   47.14    | dest_coeff sign t =
   47.15 -    let val ts = sort Term.term_ord (dest_prod t)
   47.16 +    let val ts = sort TermOrd.term_ord (dest_prod t)
   47.17          val (n, ts') = find_first_numeral [] ts
   47.18                            handle TERM _ => (1, ts)
   47.19      in (sign*n, mk_prod ts') end;