src/Pure/library.ML
changeset 36692 54b64d4ad524
parent 35976 ea3d4691a8c6
child 37851 1ce77362598f
     1.1 --- a/src/Pure/library.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/Pure/library.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  infix 2 ?
     1.5  infix 3 o oo ooo oooo
     1.6  infix 4 ~~ upto downto
     1.7 -infix orf andf mem mem_int mem_string
     1.8 +infix orf andf
     1.9  
    1.10  signature BASIC_LIBRARY =
    1.11  sig
    1.12 @@ -164,9 +164,6 @@
    1.13    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
    1.14    val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
    1.15    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.16 -  val mem: ''a * ''a list -> bool
    1.17 -  val mem_int: int * int list -> bool
    1.18 -  val mem_string: string * string list -> bool
    1.19    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.20    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.21    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    1.22 @@ -801,13 +798,6 @@
    1.23    else fold_rev (insert eq) ys xs;
    1.24  
    1.25  
    1.26 -(* old-style infixes *)
    1.27 -
    1.28 -fun x mem xs = member (op =) xs x;
    1.29 -fun (x: int) mem_int xs = member (op =) xs x;
    1.30 -fun (x: string) mem_string xs = member (op =) xs x;
    1.31 -
    1.32 -
    1.33  (* subset and set equality *)
    1.34  
    1.35  fun subset eq (xs, ys) = forall (member eq ys) xs;