--- a/src/Pure/sorts.ML Fri Sep 26 14:53:10 2008 +0200
+++ b/src/Pure/sorts.ML Fri Sep 26 17:24:15 2008 +0200
@@ -15,6 +15,7 @@
signature SORTS =
sig
+ 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
@@ -67,6 +68,7 @@
(** ordered lists of sorts **)
+val op subset = OrdList.subset Term.sort_ord;
val op union = OrdList.union Term.sort_ord;
val subtract = OrdList.subtract Term.sort_ord;