added remove_sort;
authorwenzelm
Tue Apr 25 22:23:17 2006 +0200 (2006-04-25)
changeset 194636cb10eea48c3
parent 19462 26d5f3bcc933
child 19464 d13309e30aba
added remove_sort;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Tue Apr 25 22:23:11 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Tue Apr 25 22:23:17 2006 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val eq_set: sort list * sort list -> bool
     1.5    val union: sort list -> sort list -> sort list
     1.6    val subtract: sort list -> sort list -> sort list
     1.7 +  val remove_sort: sort -> sort list -> sort list
     1.8    val insert_sort: sort -> sort list -> sort list
     1.9    val insert_typ: typ -> sort list -> sort list
    1.10    val insert_typs: typ list -> sort list -> sort list
    1.11 @@ -60,6 +61,7 @@
    1.12  val op union = OrdList.union Term.sort_ord;
    1.13  val subtract = OrdList.subtract Term.sort_ord;
    1.14  
    1.15 +val remove_sort = OrdList.remove Term.sort_ord;
    1.16  val insert_sort = OrdList.insert Term.sort_ord;
    1.17  
    1.18  fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss