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;