src/Pure/sorts.ML
changeset 29269 5c25a2012975
parent 28922 ac2c34cad840
child 29972 aee7610106fd
child 30240 5b25fee0362c
--- a/src/Pure/sorts.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/sorts.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/sorts.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 The order-sorted algebra of type classes.
@@ -74,13 +73,13 @@
 
 (** ordered lists of sorts **)
 
-val make = OrdList.make Term.sort_ord;
-val op subset = OrdList.subset Term.sort_ord;
-val op union = OrdList.union Term.sort_ord;
-val subtract = OrdList.subtract Term.sort_ord;
+val make = OrdList.make TermOrd.sort_ord;
+val op subset = OrdList.subset TermOrd.sort_ord;
+val op union = OrdList.union TermOrd.sort_ord;
+val subtract = OrdList.subtract TermOrd.sort_ord;
 
-val remove_sort = OrdList.remove Term.sort_ord;
-val insert_sort = OrdList.insert Term.sort_ord;
+val remove_sort = OrdList.remove TermOrd.sort_ord;
+val insert_sort = OrdList.insert TermOrd.sort_ord;
 
 fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
   | insert_typ (TVar (_, S)) Ss = insert_sort S Ss