modernized structure Ord_List;
authorwenzelm
Fri Sep 24 15:53:13 2010 +0200 (2010-09-24)
changeset 396874e9b6ada3a21
parent 39686 8b9f971ace20
child 39688 a6e703a1fb4f
modernized structure Ord_List;
doc-src/IsarImplementation/Thy/Prelim.thy
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/SMT/smt_monomorph.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/sat_solver.ML
src/Pure/General/ord_list.ML
src/Pure/old_term.ML
src/Pure/proofterm.ML
src/Pure/sorts.ML
src/Pure/thm.ML
src/Pure/variable.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Sep 24 15:37:36 2010 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Sep 24 15:53:13 2010 +0200
     1.3 @@ -432,30 +432,30 @@
     1.4  
     1.5    structure Terms = Theory_Data
     1.6    (
     1.7 -    type T = term OrdList.T;
     1.8 +    type T = term Ord_List.T;
     1.9      val empty = [];
    1.10      val extend = I;
    1.11      fun merge (ts1, ts2) =
    1.12 -      OrdList.union Term_Ord.fast_term_ord ts1 ts2;
    1.13 +      Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
    1.14    )
    1.15  
    1.16    val get = Terms.get;
    1.17  
    1.18    fun add raw_t thy =
    1.19      let val t = Sign.cert_term thy raw_t
    1.20 -    in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
    1.21 +    in Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy end;
    1.22  
    1.23    end;
    1.24  *}
    1.25  
    1.26 -text {* We use @{ML_type "term OrdList.T"} for reasonably efficient
    1.27 +text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient
    1.28    representation of a set of terms: all operations are linear in the
    1.29    number of stored elements.  Here we assume that our users do not
    1.30    care about the declaration order, since that data structure forces
    1.31    its own arrangement of elements.
    1.32  
    1.33    Observe how the @{verbatim merge} operation joins the data slots of
    1.34 -  the two constituents: @{ML OrdList.union} prevents duplication of
    1.35 +  the two constituents: @{ML Ord_List.union} prevents duplication of
    1.36    common data from different branches, thus avoiding the danger of
    1.37    exponential blowup.  (Plain list append etc.\ must never be used for
    1.38    theory data merges.)
     2.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Sep 24 15:37:36 2010 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Sep 24 15:53:13 2010 +0200
     2.3 @@ -275,14 +275,14 @@
     2.4  
     2.5  structure Filters = Theory_Data
     2.6  (
     2.7 -  type T = (serial * (term -> bool)) OrdList.T
     2.8 +  type T = (serial * (term -> bool)) Ord_List.T
     2.9    val empty = []
    2.10    val extend = I
    2.11 -  fun merge (fs1, fs2) = fold (OrdList.insert serial_ord) fs2 fs1
    2.12 +  fun merge (fs1, fs2) = fold (Ord_List.insert serial_ord) fs2 fs1
    2.13  )
    2.14  
    2.15  fun add_assertion_filter f =
    2.16 -  Filters.map (OrdList.insert serial_ord (serial (), f))
    2.17 +  Filters.map (Ord_List.insert serial_ord (serial (), f))
    2.18  
    2.19  fun filter_assertions thy =
    2.20    let
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 24 15:37:36 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 24 15:53:13 2010 +0200
     3.3 @@ -1254,9 +1254,9 @@
     3.4  fun partition_axioms_by_definitionality ctxt axioms def_names =
     3.5    let
     3.6      val axioms = sort (fast_string_ord o pairself fst) axioms
     3.7 -    val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
     3.8 +    val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
     3.9      val nondefs =
    3.10 -      OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
    3.11 +      Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
    3.12        |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
    3.13    in pairself (map snd) (defs, nondefs) end
    3.14  
    3.15 @@ -1289,7 +1289,7 @@
    3.16        #> filter_out (is_class_axiom o snd)
    3.17      val specs = Defs.all_specifications_of (Theory.defs_of thy)
    3.18      val def_names = specs |> maps snd |> map_filter #def
    3.19 -                    |> OrdList.make fast_string_ord
    3.20 +                    |> Ord_List.make fast_string_ord
    3.21      val thys = thy :: Theory.ancestors_of thy
    3.22      val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
    3.23      val built_in_axioms = axioms_of_thys built_in_thys
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Sep 24 15:37:36 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Sep 24 15:53:13 2010 +0200
     4.3 @@ -687,7 +687,7 @@
     4.4        | call_sets [] uss vs = vs :: call_sets uss [] []
     4.5        | call_sets ([] :: _) _ _ = []
     4.6        | call_sets ((t :: ts) :: tss) uss vs =
     4.7 -        OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
     4.8 +        Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
     4.9      val sets = call_sets (fun_calls t [] []) [] []
    4.10      val indexed_sets = sets ~~ (index_seq 0 (length sets))
    4.11    in
    4.12 @@ -701,7 +701,7 @@
    4.13    end
    4.14  fun static_args_in_terms hol_ctxt x =
    4.15    map (static_args_in_term hol_ctxt x)
    4.16 -  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
    4.17 +  #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
    4.18  
    4.19  fun overlapping_indices [] _ = []
    4.20    | overlapping_indices _ [] = []
    4.21 @@ -844,7 +844,7 @@
    4.22      fun generality (js, _, _) = ~(length js)
    4.23      fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
    4.24        x1 <> x2 andalso length j2 < length j1 andalso
    4.25 -      OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
    4.26 +      Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
    4.27      fun do_pass_1 _ [] [_] [_] = I
    4.28        | do_pass_1 T skipped _ [] = do_pass_2 T skipped
    4.29        | do_pass_1 T skipped all (z :: zs) =
     5.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Sep 24 15:37:36 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Sep 24 15:53:13 2010 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4  fun add_consts f =
     5.5    collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
     5.6  
     5.7 -val insert_const = OrdList.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
     5.8 +val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
     5.9  fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
    5.10  
    5.11  
     6.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 24 15:37:36 2010 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 24 15:53:13 2010 +0200
     6.3 @@ -136,10 +136,10 @@
     6.4    type T = (int * builtins) list
     6.5    val empty = []
     6.6    val extend = I
     6.7 -  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
     6.8 +  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
     6.9  )
    6.10  
    6.11 -fun add_builtins bs = Builtins.map (OrdList.insert fst_int_ord (serial (), bs))
    6.12 +fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
    6.13  
    6.14  fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
    6.15  
    6.16 @@ -212,10 +212,10 @@
    6.17    type T = (int * (term list -> string option)) list
    6.18    val empty = []
    6.19    val extend = I
    6.20 -  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
    6.21 +  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
    6.22  )
    6.23  
    6.24 -fun add_logic l = Logics.map (OrdList.insert fst_int_ord (serial (), l))
    6.25 +fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
    6.26  
    6.27  fun choose_logic ctxt ts =
    6.28    let
     7.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 24 15:37:36 2010 +0200
     7.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 24 15:53:13 2010 +0200
     7.3 @@ -43,11 +43,11 @@
     7.4    type T = (int * builtin_fun) list
     7.5    val empty = []
     7.6    val extend = I
     7.7 -  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
     7.8 +  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
     7.9  )
    7.10  
    7.11  fun add_builtin_funs b =
    7.12 -  Builtins.map (OrdList.insert fst_int_ord (serial (), b))
    7.13 +  Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
    7.14  
    7.15  fun get_builtin_funs ctxt c ts =
    7.16    let
    7.17 @@ -143,11 +143,11 @@
    7.18    type T = (int * mk_builtins) list
    7.19    val empty = []
    7.20    val extend = I
    7.21 -  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
    7.22 +  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
    7.23  )
    7.24  
    7.25  fun add_mk_builtins mk =
    7.26 -  Mk_Builtins.map (OrdList.insert fst_int_ord (serial (), mk))
    7.27 +  Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
    7.28  
    7.29  fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
    7.30  
     8.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Sep 24 15:37:36 2010 +0200
     8.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Sep 24 15:53:13 2010 +0200
     8.3 @@ -600,7 +600,7 @@
     8.4        (* representation of clauses as ordered lists of literals (with duplicates removed) *)
     8.5        (* prop_formula -> int list *)
     8.6        fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
     8.7 -        OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
     8.8 +        Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
     8.9          | clause_to_lit_list (PropLogic.BoolVar i) =
    8.10          [i]
    8.11          | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
     9.1 --- a/src/Pure/General/ord_list.ML	Fri Sep 24 15:37:36 2010 +0200
     9.2 +++ b/src/Pure/General/ord_list.ML	Fri Sep 24 15:53:13 2010 +0200
     9.3 @@ -18,7 +18,7 @@
     9.4    val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
     9.5  end;
     9.6  
     9.7 -structure OrdList: ORD_LIST =
     9.8 +structure Ord_List: ORD_LIST =
     9.9  struct
    9.10  
    9.11  type 'a T = 'a list;
    10.1 --- a/src/Pure/old_term.ML	Fri Sep 24 15:37:36 2010 +0200
    10.2 +++ b/src/Pure/old_term.ML	Fri Sep 24 15:53:13 2010 +0200
    10.3 @@ -75,7 +75,7 @@
    10.4  
    10.5  (*Accumulates the Vars in the term, suppressing duplicates.*)
    10.6  fun add_term_vars (t, vars: term list) = case t of
    10.7 -    Var   _ => OrdList.insert Term_Ord.term_ord t vars
    10.8 +    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
    10.9    | Abs (_,_,body) => add_term_vars(body,vars)
   10.10    | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   10.11    | _ => vars;
   10.12 @@ -84,7 +84,7 @@
   10.13  
   10.14  (*Accumulates the Frees in the term, suppressing duplicates.*)
   10.15  fun add_term_frees (t, frees: term list) = case t of
   10.16 -    Free   _ => OrdList.insert Term_Ord.term_ord t frees
   10.17 +    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
   10.18    | Abs (_,_,body) => add_term_frees(body,frees)
   10.19    | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   10.20    | _ => frees;
    11.1 --- a/src/Pure/proofterm.ML	Fri Sep 24 15:37:36 2010 +0200
    11.2 +++ b/src/Pure/proofterm.ML	Fri Sep 24 15:53:13 2010 +0200
    11.3 @@ -24,8 +24,8 @@
    11.4     | Promise of serial * term * typ list
    11.5     | PThm of serial * ((string * term * typ list option) * proof_body future)
    11.6    and proof_body = PBody of
    11.7 -    {oracles: (string * term) OrdList.T,
    11.8 -     thms: (serial * (string * term * proof_body future)) OrdList.T,
    11.9 +    {oracles: (string * term) Ord_List.T,
   11.10 +     thms: (serial * (string * term * proof_body future)) Ord_List.T,
   11.11       proof: proof}
   11.12  
   11.13    val %> : proof * term -> proof
   11.14 @@ -46,9 +46,9 @@
   11.15  
   11.16    val oracle_ord: oracle * oracle -> order
   11.17    val thm_ord: pthm * pthm -> order
   11.18 -  val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
   11.19 -  val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
   11.20 -  val all_oracles_of: proof_body -> oracle OrdList.T
   11.21 +  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
   11.22 +  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
   11.23 +  val all_oracles_of: proof_body -> oracle Ord_List.T
   11.24    val approximate_proof_body: proof -> proof_body
   11.25  
   11.26    (** primitive operations **)
   11.27 @@ -163,8 +163,8 @@
   11.28   | Promise of serial * term * typ list
   11.29   | PThm of serial * ((string * term * typ list option) * proof_body future)
   11.30  and proof_body = PBody of
   11.31 -  {oracles: (string * term) OrdList.T,
   11.32 -   thms: (serial * (string * term * proof_body future)) OrdList.T,
   11.33 +  {oracles: (string * term) Ord_List.T,
   11.34 +   thms: (serial * (string * term * proof_body future)) Ord_List.T,
   11.35     proof: proof};
   11.36  
   11.37  type oracle = string * term;
   11.38 @@ -235,8 +235,8 @@
   11.39  val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
   11.40  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
   11.41  
   11.42 -val merge_oracles = OrdList.union oracle_ord;
   11.43 -val merge_thms = OrdList.union thm_ord;
   11.44 +val merge_oracles = Ord_List.union oracle_ord;
   11.45 +val merge_thms = Ord_List.union thm_ord;
   11.46  
   11.47  val all_oracles_of =
   11.48    let
   11.49 @@ -259,8 +259,8 @@
   11.50          | _ => I) [prf] ([], []);
   11.51    in
   11.52      PBody
   11.53 -     {oracles = OrdList.make oracle_ord oracles,
   11.54 -      thms = OrdList.make thm_ord thms,
   11.55 +     {oracles = Ord_List.make oracle_ord oracles,
   11.56 +      thms = Ord_List.make thm_ord thms,
   11.57        proof = prf}
   11.58    end;
   11.59  
    12.1 --- a/src/Pure/sorts.ML	Fri Sep 24 15:37:36 2010 +0200
    12.2 +++ b/src/Pure/sorts.ML	Fri Sep 24 15:53:13 2010 +0200
    12.3 @@ -14,16 +14,16 @@
    12.4  
    12.5  signature SORTS =
    12.6  sig
    12.7 -  val make: sort list -> sort OrdList.T
    12.8 -  val subset: sort OrdList.T * sort OrdList.T -> bool
    12.9 -  val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
   12.10 -  val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
   12.11 -  val remove_sort: sort -> sort OrdList.T -> sort OrdList.T
   12.12 -  val insert_sort: sort -> sort OrdList.T -> sort OrdList.T
   12.13 -  val insert_typ: typ -> sort OrdList.T -> sort OrdList.T
   12.14 -  val insert_typs: typ list -> sort OrdList.T -> sort OrdList.T
   12.15 -  val insert_term: term -> sort OrdList.T -> sort OrdList.T
   12.16 -  val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
   12.17 +  val make: sort list -> sort Ord_List.T
   12.18 +  val subset: sort Ord_List.T * sort Ord_List.T -> bool
   12.19 +  val union: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
   12.20 +  val subtract: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
   12.21 +  val remove_sort: sort -> sort Ord_List.T -> sort Ord_List.T
   12.22 +  val insert_sort: sort -> sort Ord_List.T -> sort Ord_List.T
   12.23 +  val insert_typ: typ -> sort Ord_List.T -> sort Ord_List.T
   12.24 +  val insert_typs: typ list -> sort Ord_List.T -> sort Ord_List.T
   12.25 +  val insert_term: term -> sort Ord_List.T -> sort Ord_List.T
   12.26 +  val insert_terms: term list -> sort Ord_List.T -> sort Ord_List.T
   12.27    type algebra
   12.28    val classes_of: algebra -> serial Graph.T
   12.29    val arities_of: algebra -> (class * sort list) list Symtab.table
   12.30 @@ -37,7 +37,7 @@
   12.31    val inter_sort: algebra -> sort * sort -> sort
   12.32    val minimize_sort: algebra -> sort -> sort
   12.33    val complete_sort: algebra -> sort -> sort
   12.34 -  val minimal_sorts: algebra -> sort list -> sort OrdList.T
   12.35 +  val minimal_sorts: algebra -> sort list -> sort Ord_List.T
   12.36    val certify_class: algebra -> class -> class    (*exception TYPE*)
   12.37    val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
   12.38    val add_class: Pretty.pp -> class * class list -> algebra -> algebra
   12.39 @@ -71,13 +71,13 @@
   12.40  
   12.41  (** ordered lists of sorts **)
   12.42  
   12.43 -val make = OrdList.make Term_Ord.sort_ord;
   12.44 -val subset = OrdList.subset Term_Ord.sort_ord;
   12.45 -val union = OrdList.union Term_Ord.sort_ord;
   12.46 -val subtract = OrdList.subtract Term_Ord.sort_ord;
   12.47 +val make = Ord_List.make Term_Ord.sort_ord;
   12.48 +val subset = Ord_List.subset Term_Ord.sort_ord;
   12.49 +val union = Ord_List.union Term_Ord.sort_ord;
   12.50 +val subtract = Ord_List.subtract Term_Ord.sort_ord;
   12.51  
   12.52 -val remove_sort = OrdList.remove Term_Ord.sort_ord;
   12.53 -val insert_sort = OrdList.insert Term_Ord.sort_ord;
   12.54 +val remove_sort = Ord_List.remove Term_Ord.sort_ord;
   12.55 +val insert_sort = Ord_List.insert Term_Ord.sort_ord;
   12.56  
   12.57  fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   12.58    | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
    13.1 --- a/src/Pure/thm.ML	Fri Sep 24 15:37:36 2010 +0200
    13.2 +++ b/src/Pure/thm.ML	Fri Sep 24 15:53:13 2010 +0200
    13.3 @@ -15,7 +15,7 @@
    13.4     {thy_ref: theory_ref,
    13.5      T: typ,
    13.6      maxidx: int,
    13.7 -    sorts: sort OrdList.T}
    13.8 +    sorts: sort Ord_List.T}
    13.9    val theory_of_ctyp: ctyp -> theory
   13.10    val typ_of: ctyp -> typ
   13.11    val ctyp_of: theory -> typ -> ctyp
   13.12 @@ -28,9 +28,9 @@
   13.13      t: term,
   13.14      T: typ,
   13.15      maxidx: int,
   13.16 -    sorts: sort OrdList.T}
   13.17 +    sorts: sort Ord_List.T}
   13.18    val crep_cterm: cterm ->
   13.19 -    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort OrdList.T}
   13.20 +    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
   13.21    val theory_of_cterm: cterm -> theory
   13.22    val term_of: cterm -> term
   13.23    val cterm_of: theory -> term -> cterm
   13.24 @@ -44,16 +44,16 @@
   13.25     {thy_ref: theory_ref,
   13.26      tags: Properties.T,
   13.27      maxidx: int,
   13.28 -    shyps: sort OrdList.T,
   13.29 -    hyps: term OrdList.T,
   13.30 +    shyps: sort Ord_List.T,
   13.31 +    hyps: term Ord_List.T,
   13.32      tpairs: (term * term) list,
   13.33      prop: term}
   13.34    val crep_thm: thm ->
   13.35     {thy_ref: theory_ref,
   13.36      tags: Properties.T,
   13.37      maxidx: int,
   13.38 -    shyps: sort OrdList.T,
   13.39 -    hyps: cterm OrdList.T,
   13.40 +    shyps: sort Ord_List.T,
   13.41 +    hyps: cterm Ord_List.T,
   13.42      tpairs: (cterm * cterm) list,
   13.43      prop: cterm}
   13.44    exception THM of string * int * thm list
   13.45 @@ -163,7 +163,7 @@
   13.46   {thy_ref: theory_ref,
   13.47    T: typ,
   13.48    maxidx: int,
   13.49 -  sorts: sort OrdList.T}
   13.50 +  sorts: sort Ord_List.T}
   13.51  with
   13.52  
   13.53  fun rep_ctyp (Ctyp args) = args;
   13.54 @@ -191,7 +191,7 @@
   13.55    t: term,
   13.56    T: typ,
   13.57    maxidx: int,
   13.58 -  sorts: sort OrdList.T}
   13.59 +  sorts: sort Ord_List.T}
   13.60  with
   13.61  
   13.62  exception CTERM of string * cterm list;
   13.63 @@ -339,12 +339,12 @@
   13.64   {thy_ref: theory_ref,                          (*dynamic reference to theory*)
   13.65    tags: Properties.T,                           (*additional annotations/comments*)
   13.66    maxidx: int,                                  (*maximum index of any Var or TVar*)
   13.67 -  shyps: sort OrdList.T,                        (*sort hypotheses*)
   13.68 -  hyps: term OrdList.T,                         (*hypotheses*)
   13.69 +  shyps: sort Ord_List.T,                        (*sort hypotheses*)
   13.70 +  hyps: term Ord_List.T,                         (*hypotheses*)
   13.71    tpairs: (term * term) list,                   (*flex-flex pairs*)
   13.72    prop: term}                                   (*conclusion*)
   13.73  and deriv = Deriv of
   13.74 - {promises: (serial * thm future) OrdList.T,
   13.75 + {promises: (serial * thm future) Ord_List.T,
   13.76    body: Proofterm.proof_body}
   13.77  with
   13.78  
   13.79 @@ -380,9 +380,9 @@
   13.80  
   13.81  fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
   13.82  
   13.83 -val union_hyps = OrdList.union Term_Ord.fast_term_ord;
   13.84 -val insert_hyps = OrdList.insert Term_Ord.fast_term_ord;
   13.85 -val remove_hyps = OrdList.remove Term_Ord.fast_term_ord;
   13.86 +val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
   13.87 +val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
   13.88 +val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
   13.89  
   13.90  
   13.91  (* merge theories of cterms/thms -- trivial absorption only *)
   13.92 @@ -493,7 +493,7 @@
   13.93      (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
   13.94      (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   13.95    let
   13.96 -    val ps = OrdList.union promise_ord ps1 ps2;
   13.97 +    val ps = Ord_List.union promise_ord ps1 ps2;
   13.98      val oras = Proofterm.merge_oracles oras1 oras2;
   13.99      val thms = Proofterm.merge_thms thms1 thms2;
  13.100      val prf =
    14.1 --- a/src/Pure/variable.ML	Fri Sep 24 15:37:36 2010 +0200
    14.2 +++ b/src/Pure/variable.ML	Fri Sep 24 15:53:13 2010 +0200
    14.3 @@ -77,7 +77,7 @@
    14.4    binds: (typ * term) Vartab.table,     (*term bindings*)
    14.5    type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
    14.6    maxidx: int,                          (*maximum var index*)
    14.7 -  sorts: sort OrdList.T,                (*declared sort occurrences*)
    14.8 +  sorts: sort Ord_List.T,                (*declared sort occurrences*)
    14.9    constraints:
   14.10      typ Vartab.table *                  (*type constraints*)
   14.11      sort Vartab.table};                 (*default sorts*)