src/Pure/library.ML

   mem mem_int mem_string union union_int union_string inter inter_int
   inter_string subset subset_int subset_string;
 
 infix 3 oo ooo oooo;
 
-signature LIBRARY =
+signature BASIC_LIBRARY =
 sig
   (*functions*)
   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   val I: 'a -> 'a

   val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val \ : ''a list * ''a -> ''a list
   val \\ : ''a list * ''a list -> ''a list
   val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
   val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
+  val gen_remove: ('a * 'b -> bool) -> 'b -> 'a list -> 'a list
+  val remove: ''a -> ''a list -> ''a list
   val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   val distinct: ''a list -> ''a list
   val findrep: ''a list -> ''a list
   val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val duplicates: ''a list -> ''a list

   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val gensym: string -> string
   val scanwords: (string -> bool) -> string list -> string list
 end;
 
-signature LIBRARY_CLOSED =
+signature LIBRARY =
 sig
-  include LIBRARY
+  include BASIC_LIBRARY
 
   val the: 'a option -> 'a
   val if_none: 'a option -> 'a -> 'a
   val is_some: 'a option -> bool
   val apsome: ('a -> 'b) -> 'a option -> 'b option

   val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
   val filter: ('a -> bool) -> 'a list -> 'a list
   val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
 end;
 
-structure Library: LIBRARY_CLOSED =
+structure Library: LIBRARY =
 struct
 
 
 (** functions **)
 

 
 (*removing an element from a list -- possibly WITH duplicates*)
 fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
 fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
 
+fun gen_remove eq x xs = gen_rem eq (xs, x);
+fun remove x xs = gen_rem (op =) (xs, x);
 
 (*makes a list of the distinct members of the input; preserves order, takes
   first of equal elements*)
 fun gen_distinct eq lst =
   let

   in scan1 (#2 (take_prefix (not o is_let) cs)) end;
 
 
 end;
 
-structure OpenLibrary: LIBRARY = Library;
-open OpenLibrary;
+structure BasicLibrary: BASIC_LIBRARY = Library;
+open BasicLibrary;