--- 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,