src/Pure/sorts.ML
changeset 28354 c5fe7372ae4e
parent 27555 dfda3192dec2
child 28374 27f1b5cc5f9b
     1.1 --- a/src/Pure/sorts.ML	Thu Sep 25 11:14:01 2008 +0200
     1.2 +++ b/src/Pure/sorts.ML	Thu Sep 25 13:21:13 2008 +0200
     1.3 @@ -15,14 +15,14 @@
     1.4  
     1.5  signature SORTS =
     1.6  sig
     1.7 -  val union: sort list -> sort list -> sort list
     1.8 -  val subtract: sort list -> sort list -> sort list
     1.9 -  val remove_sort: sort -> sort list -> sort list
    1.10 -  val insert_sort: sort -> sort list -> sort list
    1.11 -  val insert_typ: typ -> sort list -> sort list
    1.12 -  val insert_typs: typ list -> sort list -> sort list
    1.13 -  val insert_term: term -> sort list -> sort list
    1.14 -  val insert_terms: term list -> sort list -> sort list
    1.15 +  val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
    1.16 +  val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
    1.17 +  val remove_sort: sort -> sort OrdList.T -> sort OrdList.T
    1.18 +  val insert_sort: sort -> sort OrdList.T -> sort OrdList.T
    1.19 +  val insert_typ: typ -> sort OrdList.T -> sort OrdList.T
    1.20 +  val insert_typs: typ list -> sort OrdList.T -> sort OrdList.T
    1.21 +  val insert_term: term -> sort OrdList.T -> sort OrdList.T
    1.22 +  val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
    1.23    type algebra
    1.24    val rep_algebra: algebra ->
    1.25     {classes: serial Graph.T,