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