src/Pure/sorts.ML
changeset 33037 b22e44496dc2
parent 32791 e6d47ce70d27
child 35408 b48ab741683b
--- a/src/Pure/sorts.ML	Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/sorts.ML	Tue Oct 20 16:13:01 2009 +0200
@@ -72,8 +72,8 @@
 (** ordered lists of sorts **)
 
 val make = OrdList.make TermOrd.sort_ord;
-val op subset = OrdList.subset TermOrd.sort_ord;
-val op union = OrdList.union TermOrd.sort_ord;
+val subset = OrdList.subset TermOrd.sort_ord;
+val union = OrdList.union TermOrd.sort_ord;
 val subtract = OrdList.subtract TermOrd.sort_ord;
 
 val remove_sort = OrdList.remove TermOrd.sort_ord;