# HG changeset patch
# User wenzelm
# Date 1222341673 -7200
# Node ID c5fe7372ae4e7a45d4adaad4ef4853c485664c27
# Parent  40306cc4d16a4a7f130c403ffbb73ee1d4b917bb
explicit type OrdList.T;

diff -r 40306cc4d16a -r c5fe7372ae4e src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Thu Sep 25 11:14:01 2008 +0200
+++ b/src/Pure/General/ord_list.ML	Thu Sep 25 13:21:13 2008 +0200
@@ -8,18 +8,21 @@
 
 signature ORD_LIST =
 sig
-  val member: ('b * 'a -> order) -> 'a list -> 'b -> bool
-  val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
-  val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
-  val subset: ('b * 'a -> order) -> 'b list * 'a list -> bool
-  val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
-  val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
-  val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
+  type 'a T = 'a list
+  val member: ('b * 'a -> order) -> 'a T -> 'b -> bool
+  val insert: ('a * 'a -> order) -> 'a -> 'a T -> 'a T
+  val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
+  val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
+  val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
+  val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
+  val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
 end;
 
 structure OrdList: ORD_LIST =
 struct
 
+type 'a T = 'a list;
+
 
 (* single elements *)
 
diff -r 40306cc4d16a -r c5fe7372ae4e src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Thu Sep 25 11:14:01 2008 +0200
+++ b/src/Pure/sorts.ML	Thu Sep 25 13:21:13 2008 +0200
@@ -15,14 +15,14 @@
 
 signature SORTS =
 sig
-  val union: sort list -> sort list -> sort list
-  val subtract: sort list -> sort list -> sort list
-  val remove_sort: sort -> sort list -> sort list
-  val insert_sort: sort -> sort list -> sort list
-  val insert_typ: typ -> sort list -> sort list
-  val insert_typs: typ list -> sort list -> sort list
-  val insert_term: term -> sort list -> sort list
-  val insert_terms: term list -> sort list -> sort list
+  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
   type algebra
   val rep_algebra: algebra ->
    {classes: serial Graph.T,
diff -r 40306cc4d16a -r c5fe7372ae4e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 25 11:14:01 2008 +0200
+++ b/src/Pure/thm.ML	Thu Sep 25 13:21:13 2008 +0200
@@ -16,7 +16,7 @@
    {thy_ref: theory_ref,
     T: typ,
     maxidx: int,
-    sorts: sort list}
+    sorts: sort OrdList.T}
   val theory_of_ctyp: ctyp -> theory
   val typ_of: ctyp -> typ
   val ctyp_of: theory -> typ -> ctyp
@@ -29,8 +29,9 @@
     t: term,
     T: typ,
     maxidx: int,
-    sorts: sort list}
-  val crep_cterm: cterm -> {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort list}
+    sorts: sort OrdList.T}
+  val crep_cterm: cterm ->
+    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort OrdList.T}
   val theory_of_cterm: cterm -> theory
   val term_of: cterm -> term
   val cterm_of: theory -> term -> cterm
@@ -44,16 +45,16 @@
    {thy_ref: theory_ref,
     tags: Properties.T,
     maxidx: int,
-    shyps: sort list,
-    hyps: term list,
+    shyps: sort OrdList.T,
+    hyps: term OrdList.T,
     tpairs: (term * term) list,
     prop: term}
   val crep_thm: thm ->
    {thy_ref: theory_ref,
     tags: Properties.T,
     maxidx: int,
-    shyps: sort list,
-    hyps: cterm list,
+    shyps: sort OrdList.T,
+    hyps: cterm OrdList.T,
     tpairs: (cterm * cterm) list,
     prop: cterm}
   exception THM of string * int * thm list
@@ -128,7 +129,7 @@
   val dest_deriv: thm ->
    {oracle: bool,
     proof: Proofterm.proof,
-    promises: (serial * (thm Future.T * theory * sort list * term)) list}
+    promises: (serial * (thm Future.T * theory * sort OrdList.T * term)) OrdList.T}
   val oracle_of: thm -> bool
   val major_prem_of: thm -> term
   val no_prems: thm -> bool
@@ -171,7 +172,7 @@
  {thy_ref: theory_ref,
   T: typ,
   maxidx: int,
-  sorts: sort list}
+  sorts: sort OrdList.T}
 with
 
 fun rep_ctyp (Ctyp args) = args;
@@ -199,7 +200,7 @@
   t: term,
   T: typ,
   maxidx: int,
-  sorts: sort list}
+  sorts: sort OrdList.T}
 with
 
 exception CTERM of string * cterm list;
@@ -342,20 +343,20 @@
 (*** Derivations and Theorems ***)
 
 abstype thm = Thm of
- deriv *                               (*derivation*)
- {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 list,                    (*sort hypotheses as ordered list*)
-  hyps: term list,                     (*hypotheses as ordered list*)
-  tpairs: (term * term) list,          (*flex-flex pairs*)
-  prop: term}                          (*conclusion*)
-and deriv = Deriv of
- {oracle: bool,                        (*oracle occurrence flag*)
-  proof: Pt.proof,                     (*proof term*)
-  promises: (serial * promise) list}   (*promised derivations*)
+ deriv *                                  (*derivation*)
+ {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*)
+  tpairs: (term * term) list,             (*flex-flex pairs*)
+  prop: term}                             (*conclusion*)
+and deriv = Deriv of                
+ {oracle: bool,                           (*oracle occurrence flag*)
+  proof: Pt.proof,                        (*proof term*)
+  promises: (serial * promise) OrdList.T} (*promised derivations*)
 and promise = Promise of
-  thm Future.T * theory * sort list * term
+  thm Future.T * theory * sort OrdList.T * term
 with
 
 type conv = cterm -> thm;
@@ -388,6 +389,8 @@
 fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
 
 val union_hyps = OrdList.union Term.fast_term_ord;
+val insert_hyps = OrdList.insert Term.fast_term_ord;
+val remove_hyps = OrdList.remove Term.fast_term_ord;
 
 
 (* merge theories of cterms/thms -- trivial absorption only *)
@@ -468,7 +471,7 @@
         tags = tags,
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
-        hyps = OrdList.insert Term.fast_term_ord A hyps,
+        hyps = insert_hyps A hyps,
         tpairs = tpairs,
         prop = prop})
   end;
@@ -501,21 +504,16 @@
 
 (** derivations **)
 
-(* type deriv *)
-
 fun make_deriv oracle promises proof =
   Deriv {oracle = oracle, promises = promises, proof = proof};
 
 val empty_deriv = make_deriv false [] Pt.min_proof;
 
 
-(* type promise *)
+(* inference rules *)
 
 fun promise_ord ((i, Promise _), (j, Promise _)) = int_ord (j, i);
 
-
-(* inference rules *)
-
 fun deriv_rule2 f
     (Deriv {oracle = ora1, promises = ps1, proof = prf1})
     (Deriv {oracle = ora2, promises = ps2, proof = prf2}) =
@@ -653,7 +651,7 @@
       tags = [],
       maxidx = Int.max (maxidxA, maxidx),
       shyps = Sorts.union sorts shyps,
-      hyps = OrdList.remove Term.fast_term_ord A hyps,
+      hyps = remove_hyps A hyps,
       tpairs = tpairs,
       prop = Logic.mk_implies (A, prop)});