# HG changeset patch
# User wenzelm
# Date 1285336393 -7200
# Node ID 4e9b6ada3a21221fa97a89a5637e4841117c77a9
# Parent  8b9f971ace20edae3372722bf4bcf623c1b06217
modernized structure Ord_List;

diff -r 8b9f971ace20 -r 4e9b6ada3a21 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Sep 24 15:37:36 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Sep 24 15:53:13 2010 +0200
@@ -432,30 +432,30 @@
 
   structure Terms = Theory_Data
   (
-    type T = term OrdList.T;
+    type T = term Ord_List.T;
     val empty = [];
     val extend = I;
     fun merge (ts1, ts2) =
-      OrdList.union Term_Ord.fast_term_ord ts1 ts2;
+      Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
   )
 
   val get = Terms.get;
 
   fun add raw_t thy =
     let val t = Sign.cert_term thy raw_t
-    in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
+    in Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy end;
 
   end;
 *}
 
-text {* We use @{ML_type "term OrdList.T"} for reasonably efficient
+text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient
   representation of a set of terms: all operations are linear in the
   number of stored elements.  Here we assume that our users do not
   care about the declaration order, since that data structure forces
   its own arrangement of elements.
 
   Observe how the @{verbatim merge} operation joins the data slots of
-  the two constituents: @{ML OrdList.union} prevents duplication of
+  the two constituents: @{ML Ord_List.union} prevents duplication of
   common data from different branches, thus avoiding the danger of
   exponential blowup.  (Plain list append etc.\ must never be used for
   theory data merges.)
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -275,14 +275,14 @@
 
 structure Filters = Theory_Data
 (
-  type T = (serial * (term -> bool)) OrdList.T
+  type T = (serial * (term -> bool)) Ord_List.T
   val empty = []
   val extend = I
-  fun merge (fs1, fs2) = fold (OrdList.insert serial_ord) fs2 fs1
+  fun merge (fs1, fs2) = fold (Ord_List.insert serial_ord) fs2 fs1
 )
 
 fun add_assertion_filter f =
-  Filters.map (OrdList.insert serial_ord (serial (), f))
+  Filters.map (Ord_List.insert serial_ord (serial (), f))
 
 fun filter_assertions thy =
   let
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -1254,9 +1254,9 @@
 fun partition_axioms_by_definitionality ctxt axioms def_names =
   let
     val axioms = sort (fast_string_ord o pairself fst) axioms
-    val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
+    val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
     val nondefs =
-      OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
+      Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
       |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
   in pairself (map snd) (defs, nondefs) end
 
@@ -1289,7 +1289,7 @@
       #> filter_out (is_class_axiom o snd)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)
     val def_names = specs |> maps snd |> map_filter #def
-                    |> OrdList.make fast_string_ord
+                    |> Ord_List.make fast_string_ord
     val thys = thy :: Theory.ancestors_of thy
     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
     val built_in_axioms = axioms_of_thys built_in_thys
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -687,7 +687,7 @@
       | call_sets [] uss vs = vs :: call_sets uss [] []
       | call_sets ([] :: _) _ _ = []
       | call_sets ((t :: ts) :: tss) uss vs =
-        OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
+        Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
     val sets = call_sets (fun_calls t [] []) [] []
     val indexed_sets = sets ~~ (index_seq 0 (length sets))
   in
@@ -701,7 +701,7 @@
   end
 fun static_args_in_terms hol_ctxt x =
   map (static_args_in_term hol_ctxt x)
-  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
+  #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
 
 fun overlapping_indices [] _ = []
   | overlapping_indices _ [] = []
@@ -844,7 +844,7 @@
     fun generality (js, _, _) = ~(length js)
     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
       x1 <> x2 andalso length j2 < length j1 andalso
-      OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
+      Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
     fun do_pass_1 _ [] [_] [_] = I
       | do_pass_1 T skipped _ [] = do_pass_2 T skipped
       | do_pass_1 T skipped all (z :: zs) =
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -29,7 +29,7 @@
 fun add_consts f =
   collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
 
-val insert_const = OrdList.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
+val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
 fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
 
 
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -136,10 +136,10 @@
   type T = (int * builtins) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
-fun add_builtins bs = Builtins.map (OrdList.insert fst_int_ord (serial (), bs))
+fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
 
 fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
 
@@ -212,10 +212,10 @@
   type T = (int * (term list -> string option)) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
-fun add_logic l = Logics.map (OrdList.insert fst_int_ord (serial (), l))
+fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
 
 fun choose_logic ctxt ts =
   let
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -43,11 +43,11 @@
   type T = (int * builtin_fun) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
 fun add_builtin_funs b =
-  Builtins.map (OrdList.insert fst_int_ord (serial (), b))
+  Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
 
 fun get_builtin_funs ctxt c ts =
   let
@@ -143,11 +143,11 @@
   type T = (int * mk_builtins) list
   val empty = []
   val extend = I
-  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+  fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
 )
 
 fun add_mk_builtins mk =
-  Mk_Builtins.map (OrdList.insert fst_int_ord (serial (), mk))
+  Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
 
 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
 
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -600,7 +600,7 @@
       (* representation of clauses as ordered lists of literals (with duplicates removed) *)
       (* prop_formula -> int list *)
       fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
-        OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
+        Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
         | clause_to_lit_list (PropLogic.BoolVar i) =
         [i]
         | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/General/ord_list.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -18,7 +18,7 @@
   val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
 end;
 
-structure OrdList: ORD_LIST =
+structure Ord_List: ORD_LIST =
 struct
 
 type 'a T = 'a list;
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/old_term.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -75,7 +75,7 @@
 
 (*Accumulates the Vars in the term, suppressing duplicates.*)
 fun add_term_vars (t, vars: term list) = case t of
-    Var   _ => OrdList.insert Term_Ord.term_ord t vars
+    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
   | Abs (_,_,body) => add_term_vars(body,vars)
   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   | _ => vars;
@@ -84,7 +84,7 @@
 
 (*Accumulates the Frees in the term, suppressing duplicates.*)
 fun add_term_frees (t, frees: term list) = case t of
-    Free   _ => OrdList.insert Term_Ord.term_ord t frees
+    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
   | Abs (_,_,body) => add_term_frees(body,frees)
   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   | _ => frees;
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/proofterm.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -24,8 +24,8 @@
    | Promise of serial * term * typ list
    | PThm of serial * ((string * term * typ list option) * proof_body future)
   and proof_body = PBody of
-    {oracles: (string * term) OrdList.T,
-     thms: (serial * (string * term * proof_body future)) OrdList.T,
+    {oracles: (string * term) Ord_List.T,
+     thms: (serial * (string * term * proof_body future)) Ord_List.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -46,9 +46,9 @@
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
-  val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
-  val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
-  val all_oracles_of: proof_body -> oracle OrdList.T
+  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
+  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
+  val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
 
   (** primitive operations **)
@@ -163,8 +163,8 @@
  | Promise of serial * term * typ list
  | PThm of serial * ((string * term * typ list option) * proof_body future)
 and proof_body = PBody of
-  {oracles: (string * term) OrdList.T,
-   thms: (serial * (string * term * proof_body future)) OrdList.T,
+  {oracles: (string * term) Ord_List.T,
+   thms: (serial * (string * term * proof_body future)) Ord_List.T,
    proof: proof};
 
 type oracle = string * term;
@@ -235,8 +235,8 @@
 val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
 fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
 
-val merge_oracles = OrdList.union oracle_ord;
-val merge_thms = OrdList.union thm_ord;
+val merge_oracles = Ord_List.union oracle_ord;
+val merge_thms = Ord_List.union thm_ord;
 
 val all_oracles_of =
   let
@@ -259,8 +259,8 @@
         | _ => I) [prf] ([], []);
   in
     PBody
-     {oracles = OrdList.make oracle_ord oracles,
-      thms = OrdList.make thm_ord thms,
+     {oracles = Ord_List.make oracle_ord oracles,
+      thms = Ord_List.make thm_ord thms,
       proof = prf}
   end;
 
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/sorts.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -14,16 +14,16 @@
 
 signature SORTS =
 sig
-  val make: sort list -> sort OrdList.T
-  val subset: sort OrdList.T * sort OrdList.T -> bool
-  val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
-  val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
-  val remove_sort: sort -> sort OrdList.T -> sort OrdList.T
-  val insert_sort: sort -> sort OrdList.T -> sort OrdList.T
-  val insert_typ: typ -> sort OrdList.T -> sort OrdList.T
-  val insert_typs: typ list -> sort OrdList.T -> sort OrdList.T
-  val insert_term: term -> sort OrdList.T -> sort OrdList.T
-  val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
+  val make: sort list -> sort Ord_List.T
+  val subset: sort Ord_List.T * sort Ord_List.T -> bool
+  val union: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+  val subtract: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+  val remove_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+  val insert_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+  val insert_typ: typ -> sort Ord_List.T -> sort Ord_List.T
+  val insert_typs: typ list -> sort Ord_List.T -> sort Ord_List.T
+  val insert_term: term -> sort Ord_List.T -> sort Ord_List.T
+  val insert_terms: term list -> sort Ord_List.T -> sort Ord_List.T
   type algebra
   val classes_of: algebra -> serial Graph.T
   val arities_of: algebra -> (class * sort list) list Symtab.table
@@ -37,7 +37,7 @@
   val inter_sort: algebra -> sort * sort -> sort
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
-  val minimal_sorts: algebra -> sort list -> sort OrdList.T
+  val minimal_sorts: algebra -> sort list -> sort Ord_List.T
   val certify_class: algebra -> class -> class    (*exception TYPE*)
   val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
   val add_class: Pretty.pp -> class * class list -> algebra -> algebra
@@ -71,13 +71,13 @@
 
 (** ordered lists of sorts **)
 
-val make = OrdList.make Term_Ord.sort_ord;
-val subset = OrdList.subset Term_Ord.sort_ord;
-val union = OrdList.union Term_Ord.sort_ord;
-val subtract = OrdList.subtract Term_Ord.sort_ord;
+val make = Ord_List.make Term_Ord.sort_ord;
+val subset = Ord_List.subset Term_Ord.sort_ord;
+val union = Ord_List.union Term_Ord.sort_ord;
+val subtract = Ord_List.subtract Term_Ord.sort_ord;
 
-val remove_sort = OrdList.remove Term_Ord.sort_ord;
-val insert_sort = OrdList.insert Term_Ord.sort_ord;
+val remove_sort = Ord_List.remove Term_Ord.sort_ord;
+val insert_sort = Ord_List.insert Term_Ord.sort_ord;
 
 fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/thm.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -15,7 +15,7 @@
    {thy_ref: theory_ref,
     T: typ,
     maxidx: int,
-    sorts: sort OrdList.T}
+    sorts: sort Ord_List.T}
   val theory_of_ctyp: ctyp -> theory
   val typ_of: ctyp -> typ
   val ctyp_of: theory -> typ -> ctyp
@@ -28,9 +28,9 @@
     t: term,
     T: typ,
     maxidx: int,
-    sorts: sort OrdList.T}
+    sorts: sort Ord_List.T}
   val crep_cterm: cterm ->
-    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort OrdList.T}
+    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
   val theory_of_cterm: cterm -> theory
   val term_of: cterm -> term
   val cterm_of: theory -> term -> cterm
@@ -44,16 +44,16 @@
    {thy_ref: theory_ref,
     tags: Properties.T,
     maxidx: int,
-    shyps: sort OrdList.T,
-    hyps: term OrdList.T,
+    shyps: sort Ord_List.T,
+    hyps: term Ord_List.T,
     tpairs: (term * term) list,
     prop: term}
   val crep_thm: thm ->
    {thy_ref: theory_ref,
     tags: Properties.T,
     maxidx: int,
-    shyps: sort OrdList.T,
-    hyps: cterm OrdList.T,
+    shyps: sort Ord_List.T,
+    hyps: cterm Ord_List.T,
     tpairs: (cterm * cterm) list,
     prop: cterm}
   exception THM of string * int * thm list
@@ -163,7 +163,7 @@
  {thy_ref: theory_ref,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T}
+  sorts: sort Ord_List.T}
 with
 
 fun rep_ctyp (Ctyp args) = args;
@@ -191,7 +191,7 @@
   t: term,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T}
+  sorts: sort Ord_List.T}
 with
 
 exception CTERM of string * cterm list;
@@ -339,12 +339,12 @@
  {thy_ref: theory_ref,                          (*dynamic reference to theory*)
   tags: Properties.T,                           (*additional annotations/comments*)
   maxidx: int,                                  (*maximum index of any Var or TVar*)
-  shyps: sort OrdList.T,                        (*sort hypotheses*)
-  hyps: term OrdList.T,                         (*hypotheses*)
+  shyps: sort Ord_List.T,                        (*sort hypotheses*)
+  hyps: term Ord_List.T,                         (*hypotheses*)
   tpairs: (term * term) list,                   (*flex-flex pairs*)
   prop: term}                                   (*conclusion*)
 and deriv = Deriv of
- {promises: (serial * thm future) OrdList.T,
+ {promises: (serial * thm future) Ord_List.T,
   body: Proofterm.proof_body}
 with
 
@@ -380,9 +380,9 @@
 
 fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
 
-val union_hyps = OrdList.union Term_Ord.fast_term_ord;
-val insert_hyps = OrdList.insert Term_Ord.fast_term_ord;
-val remove_hyps = OrdList.remove Term_Ord.fast_term_ord;
+val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
+val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
+val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
 
 
 (* merge theories of cterms/thms -- trivial absorption only *)
@@ -493,7 +493,7 @@
     (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
     (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   let
-    val ps = OrdList.union promise_ord ps1 ps2;
+    val ps = Ord_List.union promise_ord ps1 ps2;
     val oras = Proofterm.merge_oracles oras1 oras2;
     val thms = Proofterm.merge_thms thms1 thms2;
     val prf =
diff -r 8b9f971ace20 -r 4e9b6ada3a21 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/variable.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -77,7 +77,7 @@
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
   maxidx: int,                          (*maximum var index*)
-  sorts: sort OrdList.T,                (*declared sort occurrences*)
+  sorts: sort Ord_List.T,                (*declared sort occurrences*)
   constraints:
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)