member (op =);
authorwenzelm
Thu Sep 21 19:04:20 2006 +0200 (2006-09-21)
changeset 20664ffbc5a57191a
parent 20663 2024d9f7df9c
child 20665 7e54c7cc72a5
member (op =);
src/Provers/IsaPlanner/rw_inst.ML
src/Provers/blast.ML
src/Provers/splitter.ML
src/Pure/General/output.ML
src/Pure/Isar/args.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/session.ML
src/Pure/Isar/toplevel.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Thy/thy_info.ML
src/Pure/proof_general.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/tctical.ML
src/Pure/term.ML
src/Pure/unify.ML
     1.1 --- a/src/Provers/IsaPlanner/rw_inst.ML	Thu Sep 21 19:04:12 2006 +0200
     1.2 +++ b/src/Provers/IsaPlanner/rw_inst.ML	Thu Sep 21 19:04:20 2006 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4                         Term.add_term_tfrees (t,tfrees)))
     1.5                    ([],[]) ts;
     1.6          val unfixed_tvars = 
     1.7 -            List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
     1.8 +            List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
     1.9          val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
    1.10      in (fixtyinsts, tfrees) end;
    1.11  
     2.1 --- a/src/Provers/blast.ML	Thu Sep 21 19:04:12 2006 +0200
     2.2 +++ b/src/Provers/blast.ML	Thu Sep 21 19:04:20 2006 +0200
     2.3 @@ -293,7 +293,7 @@
     2.4    | Abs (a,body) =>     (*eta-contract if possible*)
     2.5          (case wkNormAux body of
     2.6               nb as (f $ t) =>
     2.7 -                 if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
     2.8 +                 if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0
     2.9                   then Abs(a,nb)
    2.10                   else wkNorm (incr_boundvars ~1 f)
    2.11             | nb => Abs (a,nb))
    2.12 @@ -385,7 +385,7 @@
    2.13          | from (Term.Abs (a,_,u)) =
    2.14                (case  from u  of
    2.15                  u' as (f $ Bound 0) =>
    2.16 -                  if (0 mem_int loose_bnos f) then Abs(a,u')
    2.17 +                  if member (op =) (loose_bnos f) 0 then Abs(a,u')
    2.18                    else incr_boundvars ~1 f
    2.19                | u' => Abs(a,u'))
    2.20          | from (Term.$ (f,u)) = from f $ from u
    2.21 @@ -679,7 +679,7 @@
    2.22  (*Eta-contract a term from outside: just enough to reduce it to an atom*)
    2.23  fun eta_contract_atom (t0 as Abs(a, body)) =
    2.24        (case  eta_contract2 body  of
    2.25 -        f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
    2.26 +        f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0
    2.27                         else eta_contract_atom (incr_boundvars ~1 f)
    2.28        | _ => t0)
    2.29    | eta_contract_atom t = t
    2.30 @@ -1178,8 +1178,8 @@
    2.31  
    2.32  (*List of variables not appearing as arguments to the given parameter*)
    2.33  fun getVars []                  i = []
    2.34 -  | getVars ((_,(v,is))::alist) i =
    2.35 -        if i mem is then getVars alist i
    2.36 +  | getVars ((_,(v,is))::alist) (i: int) =
    2.37 +        if member (op =) is i then getVars alist i
    2.38          else v :: getVars alist i;
    2.39  
    2.40  exception TRANS of string;
     3.1 --- a/src/Provers/splitter.ML	Thu Sep 21 19:04:12 2006 +0200
     3.2 +++ b/src/Provers/splitter.ML	Thu Sep 21 19:04:20 2006 +0200
     3.3 @@ -165,7 +165,7 @@
     3.4     has a body of type T; otherwise the expansion thm will fail later on
     3.5  *)
     3.6  fun type_test (T,lbnos,apsns) =
     3.7 -  let val (_,U,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
     3.8 +  let val (_,U: typ,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
     3.9    in T=U end;
    3.10  
    3.11  (*************************************************************************
    3.12 @@ -196,7 +196,7 @@
    3.13            lifting is required before applying the split-theorem.
    3.14  ******************************************************************************)
    3.15  
    3.16 -fun mk_split_pack (thm, T, T', n, ts, apsns, pos, TB, t) =
    3.17 +fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) =
    3.18    if n > length ts then []
    3.19    else let val lev = length apsns
    3.20             val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
    3.21 @@ -398,9 +398,8 @@
    3.22    | split_asm_tac splits =
    3.23  
    3.24    let val cname_list = map (fst o fst o split_thm_info) splits;
    3.25 -      fun is_case (a,_) = a mem cname_list;
    3.26        fun tac (t,i) =
    3.27 -          let val n = find_index (exists_Const is_case)
    3.28 +          let val n = find_index (exists_Const (member (op =) cname_list o #1))
    3.29                                   (Logic.strip_assums_hyp t);
    3.30                fun first_prem_is_disj (Const ("==>", _) $ (Const (c, _)
    3.31                      $ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or
     4.1 --- a/src/Pure/General/output.ML	Thu Sep 21 19:04:12 2006 +0200
     4.2 +++ b/src/Pure/General/output.ML	Thu Sep 21 19:04:20 2006 +0200
     4.3 @@ -67,7 +67,7 @@
     4.4  
     4.5  val print_mode = ref ([]: string list);
     4.6  
     4.7 -fun has_mode s = s mem_string ! print_mode;
     4.8 +fun has_mode s = member (op =) (! print_mode) s;
     4.9  
    4.10  type mode_fns =
    4.11   {output: string -> string * real,
     5.1 --- a/src/Pure/Isar/args.ML	Thu Sep 21 19:04:12 2006 +0200
     5.2 +++ b/src/Pure/Isar/args.ML	Thu Sep 21 19:04:20 2006 +0200
     5.3 @@ -349,10 +349,10 @@
     5.4  
     5.5  local
     5.6  
     5.7 -val exclude = explode "()[],";
     5.8 +val exclude = member (op =) (explode "()[],");
     5.9  
    5.10  fun atomic blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
    5.11 -    k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ","));
    5.12 +    k <> Keyword orelse not (exclude x) orelse blk andalso x = ","));
    5.13  
    5.14  fun args blk x = Scan.optional (args1 blk) [] x
    5.15  and args1 blk x =
     6.1 --- a/src/Pure/Isar/locale.ML	Thu Sep 21 19:04:12 2006 +0200
     6.2 +++ b/src/Pure/Isar/locale.ML	Thu Sep 21 19:04:20 2006 +0200
     6.3 @@ -1644,7 +1644,7 @@
     6.4  
     6.5      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
     6.6      val env = Term.add_term_free_names (body, []);
     6.7 -    val xs = filter (fn (x, _) => x mem_string env) parms;
     6.8 +    val xs = filter (member (op =) env o #1) parms;
     6.9      val Ts = map #2 xs;
    6.10      val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
    6.11        |> Library.sort_wrt #1 |> map TFree;
     7.1 --- a/src/Pure/Isar/outer_lex.ML	Thu Sep 21 19:04:12 2006 +0200
     7.2 +++ b/src/Pure/Isar/outer_lex.ML	Thu Sep 21 19:04:20 2006 +0200
     7.3 @@ -190,8 +190,7 @@
     7.4  
     7.5  (* scan symbolic idents *)
     7.6  
     7.7 -val sym_chars = explode "!#$%&*+-/<=>?@^_|~";
     7.8 -fun is_sym_char s = s mem sym_chars;
     7.9 +val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
    7.10  
    7.11  val scan_symid =
    7.12    Scan.any1 is_sym_char >> implode ||
     8.1 --- a/src/Pure/Isar/session.ML	Thu Sep 21 19:04:12 2006 +0200
     8.2 +++ b/src/Pure/Isar/session.ML	Thu Sep 21 19:04:20 2006 +0200
     8.3 @@ -50,7 +50,7 @@
     8.4  (* init *)
     8.5  
     8.6  fun init reset parent name =
     8.7 -  if not (parent mem_string (! session)) orelse not (! session_finished) then
     8.8 +  if not (member (op =) (! session) parent) orelse not (! session_finished) then
     8.9      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    8.10    else (add_path reset name; session_finished := false);
    8.11  
     9.1 --- a/src/Pure/Isar/toplevel.ML	Thu Sep 21 19:04:12 2006 +0200
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Sep 21 19:04:20 2006 +0200
     9.3 @@ -619,7 +619,7 @@
     9.4          |> (if ! profiling > 0 then do_profiling else I)
     9.5          |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
     9.6      val _ = conditional (int andalso not (! quiet) andalso
     9.7 -        exists (fn m => m mem_string print) ("" :: ! print_mode))
     9.8 +        exists (member (op =) print) ("" :: ! print_mode))
     9.9        (fn () => print_state false result);
    9.10    in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
    9.11  
    10.1 --- a/src/Pure/Proof/extraction.ML	Thu Sep 21 19:04:12 2006 +0200
    10.2 +++ b/src/Pure/Proof/extraction.ML	Thu Sep 21 19:04:20 2006 +0200
    10.3 @@ -54,10 +54,10 @@
    10.4  fun typeof_proc defaultS vs (Const ("typeof", _) $ u) =
    10.5        SOME (mk_typ (case strip_comb u of
    10.6            (Var ((a, i), _), _) =>
    10.7 -            if a mem vs then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS)
    10.8 +            if member (op =) vs a then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS)
    10.9              else nullT
   10.10          | (Free (a, _), _) =>
   10.11 -            if a mem vs then TFree ("'" ^ a, defaultS) else nullT
   10.12 +            if member (op =) vs a then TFree ("'" ^ a, defaultS) else nullT
   10.13          | _ => nullT))
   10.14    | typeof_proc _ _ _ = NONE;
   10.15  
   10.16 @@ -147,7 +147,7 @@
   10.17  
   10.18  fun relevant_vars types prop = foldr (fn
   10.19        (Var ((a, i), T), vs) => (case strip_type T of
   10.20 -        (_, Type (s, _)) => if s mem types then a :: vs else vs
   10.21 +        (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
   10.22        | _ => vs)
   10.23      | (_, vs) => vs) [] (vars_of prop);
   10.24  
   10.25 @@ -320,7 +320,7 @@
   10.26          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
   10.27        val vars = vars_of prop;
   10.28        val vars' = filter_out (fn v =>
   10.29 -        tname_of (body_type (fastype_of v)) mem rtypes) vars;
   10.30 +        member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
   10.31        val T = etype_of thy' vs [] prop;
   10.32        val (T', thw) = Type.freeze_thaw_type
   10.33          (if T = nullT then nullT else map fastype_of vars' ---> T);
   10.34 @@ -474,7 +474,7 @@
   10.35          val n = Int.min (length vars, length ts);
   10.36  
   10.37          fun add_args ((Var ((a, i), _), t), (vs', tye)) =
   10.38 -          if a mem rvs then
   10.39 +          if member (op =) rvs a then
   10.40              let val T = etype_of thy' vs Ts t
   10.41              in if T = nullT then (vs', tye)
   10.42                 else (a :: vs', (("'" ^ a, i), T) :: tye)
   10.43 @@ -483,7 +483,7 @@
   10.44  
   10.45        in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
   10.46  
   10.47 -    fun find vs = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
   10.48 +    fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
   10.49      fun find' s = map snd o List.filter (equal s o fst)
   10.50  
   10.51      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
   10.52 @@ -523,9 +523,9 @@
   10.53            let
   10.54              val (Us, T) = strip_type (fastype_of1 (Ts, t));
   10.55              val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
   10.56 -              (if tname_of T mem rtypes then t'
   10.57 +              (if member (op =) rtypes (tname_of T) then t'
   10.58                 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
   10.59 -            val u = if not (tname_of T mem rtypes) then t else
   10.60 +            val u = if not (member (op =) rtypes (tname_of T)) then t else
   10.61                let
   10.62                  val eT = etype_of thy' vs Ts t;
   10.63                  val (r, Us') = if eT = nullT then (nullt, Us) else
   10.64 @@ -628,7 +628,7 @@
   10.65        | extr d defs vs ts Ts hs (prf % SOME t) =
   10.66            let val (defs', u) = extr d defs vs (t :: ts) Ts hs prf
   10.67            in (defs',
   10.68 -            if tname_of (body_type (fastype_of1 (Ts, t))) mem rtypes then u
   10.69 +            if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
   10.70              else u $ t)
   10.71            end
   10.72  
   10.73 @@ -661,8 +661,8 @@
   10.74                        corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
   10.75  
   10.76                      val nt = Envir.beta_norm t;
   10.77 -                    val args = filter_out (fn v => tname_of (body_type
   10.78 -                      (fastype_of v)) mem rtypes) (vfs_of prop);
   10.79 +                    val args = filter_out (fn v => member (op =) rtypes
   10.80 +                      (tname_of (body_type (fastype_of v)))) (vfs_of prop);
   10.81                      val args' = List.filter (fn v => Logic.occs (v, nt)) args;
   10.82                      val t' = mkabs nt args';
   10.83                      val T = fastype_of t';
    11.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Sep 21 19:04:12 2006 +0200
    11.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Sep 21 19:04:20 2006 +0200
    11.3 @@ -223,7 +223,7 @@
    11.4        AbsP (s, t, insert_refl defs Ts prf)
    11.5    | insert_refl defs Ts prf = (case strip_combt prf of
    11.6          (PThm ((s, _), _, prop, SOME Ts), ts) =>
    11.7 -          if s mem defs then
    11.8 +          if member (op =) defs s then
    11.9              let
   11.10                val vs = vars_of prop;
   11.11                val tvars = term_tvars prop;
   11.12 @@ -246,7 +246,7 @@
   11.13        let
   11.14          val cnames = map (fst o dest_Const o fst) defs';
   11.15          val thms = maps (fn (s, ps) =>
   11.16 -            if s mem defnames then []
   11.17 +            if member (op =) defnames s then []
   11.18              else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
   11.19                null (term_consts p inter cnames)) ps))
   11.20            (Symtab.dest (thms_of_proof prf Symtab.empty))
    12.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Sep 21 19:04:12 2006 +0200
    12.2 +++ b/src/Pure/Syntax/lexicon.ML	Thu Sep 21 19:04:20 2006 +0200
    12.3 @@ -145,8 +145,7 @@
    12.4  val tvarT = Type ("tvar", []);
    12.5  
    12.6  val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
    12.7 -
    12.8 -fun is_terminal s = s mem terminals;
    12.9 +val is_terminal = member (op =) terminals;
   12.10  
   12.11  
   12.12  (* str_of_token *)
    13.1 --- a/src/Pure/Syntax/parser.ML	Thu Sep 21 19:04:12 2006 +0200
    13.2 +++ b/src/Pure/Syntax/parser.ML	Thu Sep 21 19:04:20 2006 +0200
    13.3 @@ -75,7 +75,7 @@
    13.4        (*store chain if it does not already exist*)
    13.5        val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
    13.6          let val old_tos = these (AList.lookup (op =) chains from) in
    13.7 -          if lhs mem old_tos then (NONE, chains)
    13.8 +          if member (op =) old_tos lhs then (NONE, chains)
    13.9            else (SOME from, AList.update (op =) (from, lhs ins old_tos) chains)
   13.10          end;
   13.11  
   13.12 @@ -101,13 +101,13 @@
   13.13  
   13.14              val tos = connected_with chains' [lhs] [lhs];
   13.15          in (copy_lookahead tos [],
   13.16 -            (if lhs mem lambdas then tos else []) union lambdas)
   13.17 +            (if member (op =) lambdas lhs then tos else []) union lambdas)
   13.18          end;
   13.19  
   13.20        (*test if new production can produce lambda
   13.21          (rhs must either be empty or only consist of lambda NTs)*)
   13.22        val (new_lambda, lambdas') =
   13.23 -        if forall (fn (Nonterminal (id, _)) => id mem lambdas'
   13.24 +        if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
   13.25                      | (Terminal _) => false) rhs then
   13.26            (true, lambdas' union (connected_with chains' [lhs] [lhs]))
   13.27          else
   13.28 @@ -118,7 +118,7 @@
   13.29        fun lookahead_dependency _ [] nts = (NONE, nts)
   13.30          | lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts)
   13.31          | lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts =
   13.32 -            if nt mem lambdas then
   13.33 +            if member (op =) lambdas nt then
   13.34                lookahead_dependency lambdas symbs (nt :: nts)
   13.35              else (NONE, nt :: nts);
   13.36  
   13.37 @@ -145,7 +145,7 @@
   13.38                        nt_dependencies added_tks nt_prods =
   13.39                      let val (tk, nts) = lookahead_dependency lambdas rhs [];
   13.40                      in
   13.41 -                      if l mem nts then       (*update production's lookahead*)
   13.42 +                      if member (op =) nts l then       (*update production's lookahead*)
   13.43                        let
   13.44                          val new_lambda = is_none tk andalso nts subset lambdas;
   13.45  
   13.46 @@ -248,7 +248,7 @@
   13.47            fun add_nts [] = ()
   13.48              | add_nts (nt :: nts) =
   13.49                let val ((old_nts, old_tks), ps) = Array.sub (prods, nt);
   13.50 -              in if lhs mem old_nts then ()
   13.51 +              in if member (op =) old_nts lhs then ()
   13.52                   else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
   13.53                end;
   13.54  
   13.55 @@ -273,7 +273,7 @@
   13.56                            grammar does not contain new production already*)
   13.57                          val (tk_prods', is_new') =
   13.58                            if is_some prod_count then
   13.59 -                            if new_prod mem tk_prods then (tk_prods, false)
   13.60 +                            if member (op =) tk_prods new_prod then (tk_prods, false)
   13.61                              else (new_prod :: tk_prods, true)
   13.62                            else (new_prod :: tk_prods, true);
   13.63  
   13.64 @@ -304,7 +304,7 @@
   13.65                  (*token under which old productions which
   13.66                    depend on changed_nt could be stored*)
   13.67                  val key =
   13.68 -                 case find_first (fn t => not (t mem new_tks))
   13.69 +                 case find_first (not o member (op =) new_tks)
   13.70                                   (starts_for_nt changed_nt) of
   13.71                        NONE => SOME UnknownStart
   13.72                      | t => t;
   13.73 @@ -320,13 +320,13 @@
   13.74                        val (tk, depends) = lookahead_dependency lambdas' rhs [];
   13.75  
   13.76                        (*test if this production has to be copied*)
   13.77 -                      val update = changed_nt mem depends;
   13.78 +                      val update = member (op =) depends changed_nt;
   13.79  
   13.80                        (*test if production could already be associated with
   13.81                          a member of new_tks*)
   13.82                        val lambda = length depends > 1 orelse
   13.83                                     not (null depends) andalso is_some tk
   13.84 -                                   andalso the tk mem new_tks;
   13.85 +                                   andalso member (op =) new_tks (the tk);
   13.86  
   13.87                        (*associate production with new starting tokens*)
   13.88                        fun copy [] nt_prods = nt_prods
   13.89 @@ -811,7 +811,7 @@
   13.90                      else false
   13.91                  | reduction tk minPrec checked
   13.92                              (Nonterminal (nt, nt_prec) :: _, _, prec) =
   13.93 -                  if prec >= minPrec andalso not (nt mem checked) then
   13.94 +                  if prec >= minPrec andalso not (member (op =) checked nt) then
   13.95                      let val chained = connected_with chains [nt] [nt];
   13.96                      in exists
   13.97                           (reduction tk nt_prec (chained @ checked))
    14.1 --- a/src/Pure/Syntax/syntax.ML	Thu Sep 21 19:04:12 2006 +0200
    14.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Sep 21 19:04:20 2006 +0200
    14.3 @@ -462,7 +462,7 @@
    14.4  
    14.5      fun constify (ast as Ast.Constant _) = ast
    14.6        | constify (ast as Ast.Variable x) =
    14.7 -          if x mem consts orelse NameSpace.is_qualified x then Ast.Constant x
    14.8 +          if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x
    14.9            else ast
   14.10        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   14.11    in
    15.1 --- a/src/Pure/Thy/present.ML	Thu Sep 21 19:04:12 2006 +0200
    15.2 +++ b/src/Pure/Thy/present.ML	Thu Sep 21 19:04:20 2006 +0200
    15.3 @@ -88,7 +88,7 @@
    15.4  val _ = Context.add_setup BrowserInfoData.init;
    15.5  
    15.6  fun get_info thy =
    15.7 -  if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
    15.8 +  if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
    15.9    then {name = Context.PureN, session = [], is_local = false}
   15.10    else BrowserInfoData.get thy;
   15.11  
   15.12 @@ -541,7 +541,7 @@
   15.13  
   15.14      fun known name =
   15.15        let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
   15.16 -      in fn s => s mem_string ss end;
   15.17 +      in member (op =) ss end;
   15.18      val known_syms = known "syms.lst";
   15.19      val known_ctrls = known "ctrls.lst";
   15.20  
    16.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Sep 21 19:04:12 2006 +0200
    16.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Sep 21 19:04:20 2006 +0200
    16.3 @@ -54,7 +54,7 @@
    16.4                      | NONE => [])
    16.5                   | _ => ["global"]);
    16.6              in
    16.7 -              if name mem parents' then (gra', parents union parents')
    16.8 +              if member (op =) parents' name then (gra', parents union parents')
    16.9                else (Symtab.update (name,
   16.10                  {name = Sign.base_name name, ID = name,
   16.11                   dir = space_implode "/" (session @ prefx),
    17.1 --- a/src/Pure/Thy/thy_info.ML	Thu Sep 21 19:04:12 2006 +0200
    17.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Sep 21 19:04:20 2006 +0200
    17.3 @@ -352,8 +352,8 @@
    17.4      val path = Path.expand (Path.unpack str);
    17.5      val name = Path.pack (Path.base path);
    17.6    in
    17.7 -    if name mem_string initiators then error (cycle_msg initiators) else ();
    17.8 -    if known_thy name andalso is_finished name orelse name mem_string visited then
    17.9 +    if member (op =) initiators name then error (cycle_msg initiators) else ();
   17.10 +    if known_thy name andalso is_finished name orelse member (op =) visited name then
   17.11        (visited, (true, name))
   17.12      else
   17.13        let
    18.1 --- a/src/Pure/proof_general.ML	Thu Sep 21 19:04:12 2006 +0200
    18.2 +++ b/src/Pure/proof_general.ML	Thu Sep 21 19:04:20 2006 +0200
    18.3 @@ -867,7 +867,7 @@
    18.4                 and even if we did, we'd have to mess around here a whole lot more first
    18.5                 to pick out the terms from the syntax. *)
    18.6  
    18.7 -            if (name mem plain_items) then plain_item
    18.8 +            if member (op =) plain_items name then plain_item
    18.9              else case name of
   18.10                       "text"      => comment_item
   18.11                     | "text_raw"  => comment_item
   18.12 @@ -1460,9 +1460,9 @@
   18.13  
   18.14  local
   18.15  
   18.16 -val regexp_meta = explode ".*+?[]^$";
   18.17 +val regexp_meta = member (op =) (explode ".*+?[]^$");
   18.18  val regexp_quote =
   18.19 -  implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode;
   18.20 +  implode o map (fn c => if regexp_meta c then "\\\\" ^ c else c) o explode;
   18.21  
   18.22  fun defconst name strs =
   18.23    "\n(defconst isar-keywords-" ^ name ^
    19.1 --- a/src/Pure/pure_thy.ML	Thu Sep 21 19:04:12 2006 +0200
    19.2 +++ b/src/Pure/pure_thy.ML	Thu Sep 21 19:04:20 2006 +0200
    19.3 @@ -108,7 +108,7 @@
    19.4  fun map_tags f thm =
    19.5    Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
    19.6  
    19.7 -fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
    19.8 +fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]);
    19.9  fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s'));
   19.10  
   19.11  fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
    20.1 --- a/src/Pure/sign.ML	Thu Sep 21 19:04:12 2006 +0200
    20.2 +++ b/src/Pure/sign.ML	Thu Sep 21 19:04:20 2006 +0200
    20.3 @@ -278,7 +278,7 @@
    20.4  fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
    20.5  val typ_match = Type.typ_match o tsig_of;
    20.6  val typ_unify = Type.unify o tsig_of;
    20.7 -fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
    20.8 +val is_logtype = member (op =) o Type.logical_types o tsig_of;
    20.9  
   20.10  
   20.11  (* polymorphic constants *)
   20.12 @@ -338,7 +338,7 @@
   20.13  
   20.14  fun mapping add_names f t =
   20.15    let
   20.16 -    fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
   20.17 +    fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
   20.18      val tab = map_filter f' (add_names t []);
   20.19      fun get x = the_default x (AList.lookup (op =) tab x);
   20.20    in get end;
   20.21 @@ -663,7 +663,7 @@
   20.22  
   20.23  fun add_typedecls decls thy =
   20.24    let
   20.25 -    fun type_of (a, vs, mx) =
   20.26 +    fun type_of (a, vs: string list, mx) =
   20.27        if not (has_duplicates (op =) vs) then (a, length vs, mx)
   20.28        else error ("Duplicate parameters in type declaration: " ^ quote a);
   20.29    in add_types (map type_of decls) thy end;
    21.1 --- a/src/Pure/tctical.ML	Thu Sep 21 19:04:12 2006 +0200
    21.2 +++ b/src/Pure/tctical.ML	Thu Sep 21 19:04:20 2006 +0200
    21.3 @@ -432,7 +432,7 @@
    21.4        fun swap_ctpair (t,u) = (cterm u, cterm t)
    21.5        (*Subgoal variables: make Free; lift type over params*)
    21.6        fun mk_subgoal_inst concl_vars (var as Var(v,T)) =
    21.7 -          if var mem concl_vars
    21.8 +          if member (op =) concl_vars var
    21.9            then (var, true, free_of "METAHYP2_" (v,T))
   21.10            else (var, false,
   21.11                  free_of "METAHYP2_" (v, map #2 params --->T))
    22.1 --- a/src/Pure/term.ML	Thu Sep 21 19:04:12 2006 +0200
    22.2 +++ b/src/Pure/term.ML	Thu Sep 21 19:04:20 2006 +0200
    22.3 @@ -964,7 +964,7 @@
    22.4  fun is_first_order quants =
    22.5    let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
    22.6          | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
    22.7 -            q mem_string quants  andalso   (*it is a known quantifier*)
    22.8 +            member (op =) quants q  andalso   (*it is a known quantifier*)
    22.9              not (is_funtype T)   andalso first_order1 (T::Ts) body
   22.10          | first_order1 Ts t =
   22.11              case strip_comb t of
    23.1 --- a/src/Pure/unify.ML	Thu Sep 21 19:04:12 2006 +0200
    23.2 +++ b/src/Pure/unify.ML	Thu Sep 21 19:04:20 2006 +0200
    23.3 @@ -426,7 +426,7 @@
    23.4    let val (head,args) = strip_comb t
    23.5    in
    23.6        case head of
    23.7 -    Bound i => (i-lev) mem_int banned  orelse
    23.8 +    Bound i => member (op =) banned (i-lev)  orelse
    23.9                 exists (rigid_bound (lev, banned)) args
   23.10    | Var _ => false  (*no rigid occurrences here!*)
   23.11    | Abs (_,_,u) =>
   23.12 @@ -439,7 +439,7 @@
   23.13  fun change_bnos banned =
   23.14    let fun change lev (Bound i) =
   23.15        if i<lev then Bound i
   23.16 -      else  if (i-lev) mem_int banned
   23.17 +      else  if member (op =) banned (i-lev)
   23.18        then raise CHANGE_FAIL (**flexible occurrence: give up**)
   23.19        else  Bound (i - length (List.filter (fn j => j < i-lev) banned))
   23.20    | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   23.21 @@ -500,7 +500,7 @@
   23.22  fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
   23.23    let val loot = loose_bnos t  and  loou = loose_bnos u
   23.24        fun add_index (((a,T), j), (bnos, newbinder)) =
   23.25 -            if  j mem_int loot  andalso  j mem_int loou
   23.26 +            if  member (op =) loot j  andalso  member (op =) loou j
   23.27              then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
   23.28              else  (j::bnos, newbinder);   (*remove*)
   23.29        val indices = 0 upto (length rbinder - 1);