src/Pure/library.ML
changeset 33037 b22e44496dc2
parent 32978 a473ba9a221d
child 33038 8f9594c31de4
--- a/src/Pure/library.ML	Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/library.ML	Tue Oct 20 16:13:01 2009 +0200
@@ -11,8 +11,7 @@
 infix 2 ?
 infix 3 o oo ooo oooo
 infix 4 ~~ upto downto
-infix orf andf \ \\ mem mem_int mem_string union union_int
-  union_string inter inter_int inter_string subset subset_int subset_string
+infix orf andf \ \\ mem mem_int mem_string
 
 signature BASIC_LIBRARY =
 sig
@@ -163,19 +162,8 @@
   val mem: ''a * ''a list -> bool
   val mem_int: int * int list -> bool
   val mem_string: string * string list -> bool
-  val union: ''a list * ''a list -> ''a list
-  val union_int: int list * int list -> int list
-  val union_string: string list * string list -> string list
   val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
-  val inter: ''a list * ''a list -> ''a list
-  val inter_int: int list * int list -> int list
-  val inter_string: string list * string list -> string list
-  val subset: ''a list * ''a list -> bool
-  val subset_int: int list * int list -> bool
-  val subset_string: string list * string list -> bool
-  val eq_set: ''a list * ''a list -> bool
-  val eq_set_string: string list * string list -> bool
   val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val \ : ''a list * ''a -> ''a list
@@ -811,70 +799,20 @@
 fun (x: string) mem_string xs = member (op =) xs x;
 
 (*union of sets represented as lists: no repetitions*)
-fun xs union [] = xs
-  | [] union ys = ys
-  | (x :: xs) union ys = xs union (insert (op =) x ys);
-
-(*union of sets, optimized version for ints*)
-fun (xs:int list) union_int [] = xs
-  | [] union_int ys = ys
-  | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
-
-(*union of sets, optimized version for strings*)
-fun (xs:string list) union_string [] = xs
-  | [] union_string ys = ys
-  | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
-
-(*generalized union*)
 fun gen_union eq (xs, []) = xs
   | gen_union eq ([], ys) = ys
   | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
 
-
 (*intersection*)
-fun [] inter ys = []
-  | (x :: xs) inter ys =
-      if x mem ys then x :: (xs inter ys) else xs inter ys;
-
-(*intersection, optimized version for ints*)
-fun ([]:int list) inter_int ys = []
-  | (x :: xs) inter_int ys =
-      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
-
-(*intersection, optimized version for strings *)
-fun ([]:string list) inter_string ys = []
-  | (x :: xs) inter_string ys =
-      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
-
-(*generalized intersection*)
 fun gen_inter eq ([], ys) = []
   | gen_inter eq (x::xs, ys) =
       if member eq ys x then x :: gen_inter eq (xs, ys)
       else gen_inter eq (xs, ys);
 
-
 (*subset*)
-fun [] subset ys = true
-  | (x :: xs) subset ys = x mem ys andalso xs subset ys;
-
-(*subset, optimized version for ints*)
-fun ([]: int list) subset_int ys = true
-  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
-
-(*subset, optimized version for strings*)
-fun ([]: string list) subset_string ys = true
-  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
+fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
 
 (*set equality*)
-fun eq_set (xs, ys) =
-  xs = ys orelse (xs subset ys andalso ys subset xs);
-
-(*set equality for strings*)
-fun eq_set_string ((xs: string list), ys) =
-  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
-
-fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
-
 fun gen_eq_set eq (xs, ys) =
   eq_list eq (xs, ys) orelse
     (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));