src/Pure/library.ML
changeset 15745 33bb955b2e73
parent 15696 1da4ce092c0b
child 15760 1ca99038c847
     1.1 --- a/src/Pure/library.ML	Sat Apr 16 18:55:28 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Apr 16 18:55:51 2005 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  infix 3 oo ooo oooo;
     1.6  
     1.7 -signature LIBRARY =
     1.8 +signature BASIC_LIBRARY =
     1.9  sig
    1.10    (*functions*)
    1.11    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    1.12 @@ -192,6 +192,8 @@
    1.13    val \\ : ''a list * ''a list -> ''a list
    1.14    val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
    1.15    val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    1.16 +  val gen_remove: ('a * 'b -> bool) -> 'b -> 'a list -> 'a list
    1.17 +  val remove: ''a -> ''a list -> ''a list
    1.18    val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    1.19    val distinct: ''a list -> ''a list
    1.20    val findrep: ''a list -> ''a list
    1.21 @@ -256,9 +258,9 @@
    1.22    val scanwords: (string -> bool) -> string list -> string list
    1.23  end;
    1.24  
    1.25 -signature LIBRARY_CLOSED =
    1.26 +signature LIBRARY =
    1.27  sig
    1.28 -  include LIBRARY
    1.29 +  include BASIC_LIBRARY
    1.30  
    1.31    val the: 'a option -> 'a
    1.32    val if_none: 'a option -> 'a -> 'a
    1.33 @@ -279,7 +281,7 @@
    1.34    val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
    1.35  end;
    1.36  
    1.37 -structure Library: LIBRARY_CLOSED =
    1.38 +structure Library: LIBRARY =
    1.39  struct
    1.40  
    1.41  
    1.42 @@ -933,6 +935,8 @@
    1.43  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
    1.44  fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
    1.45  
    1.46 +fun gen_remove eq x xs = gen_rem eq (xs, x);
    1.47 +fun remove x xs = gen_rem (op =) (xs, x);
    1.48  
    1.49  (*makes a list of the distinct members of the input; preserves order, takes
    1.50    first of equal elements*)
    1.51 @@ -1289,5 +1293,5 @@
    1.52  
    1.53  end;
    1.54  
    1.55 -structure OpenLibrary: LIBRARY = Library;
    1.56 -open OpenLibrary;
    1.57 +structure BasicLibrary: BASIC_LIBRARY = Library;
    1.58 +open BasicLibrary;