merged
authorhaftmann
Thu May 06 08:44:19 2010 +0200 (2010-05-06)
changeset 3669340dcc319d4cd
parent 36691 842fdcd42159
parent 36692 54b64d4ad524
child 36694 978e6469b504
merged
     1.1 --- a/src/FOLP/hypsubst.ML	Thu May 06 08:43:51 2010 +0200
     1.2 +++ b/src/FOLP/hypsubst.ML	Thu May 06 08:44:19 2010 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  exception EQ_VAR;
     1.6  
     1.7 -fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
     1.8 +fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0;
     1.9  
    1.10  (*It's not safe to substitute for a constant; consider 0=1.
    1.11    It's not safe to substitute for x=t[x] since x is not eliminated.
     2.1 --- a/src/FOLP/simp.ML	Thu May 06 08:43:51 2010 +0200
     2.2 +++ b/src/FOLP/simp.ML	Thu May 06 08:44:19 2010 +0200
     2.3 @@ -98,7 +98,7 @@
     2.4  in var(lhs_of_eq i thm) end;
     2.5  
     2.6  fun contains_op opns =
     2.7 -    let fun contains(Const(s,_)) = s mem opns |
     2.8 +    let fun contains(Const(s,_)) = member (op =) opns s |
     2.9              contains(s$t) = contains s orelse contains t |
    2.10              contains(Abs(_,_,t)) = contains t |
    2.11              contains _ = false;
    2.12 @@ -117,7 +117,7 @@
    2.13    in map norm normE_thms end;
    2.14  
    2.15  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    2.16 -        Const(s,_)$_ => s mem norms | _ => false;
    2.17 +        Const(s,_)$_ => member (op =) norms s | _ => false;
    2.18  
    2.19  val refl_tac = resolve_tac refl_thms;
    2.20  
    2.21 @@ -203,7 +203,7 @@
    2.22      val refl1_tac = refl_tac 1
    2.23      fun norm_step_tac st = st |>
    2.24           (case head_of(rhs_of_eq 1 st) of
    2.25 -            Var(ixn,_) => if ixn mem hvs then refl1_tac
    2.26 +            Var(ixn,_) => if member (op =) hvs ixn then refl1_tac
    2.27                            else resolve_tac normI_thms 1 ORELSE refl1_tac
    2.28            | Const _ => resolve_tac normI_thms 1 ORELSE
    2.29                         resolve_tac congs 1 ORELSE refl1_tac
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu May 06 08:43:51 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu May 06 08:44:19 2010 +0200
     3.3 @@ -46,7 +46,7 @@
     3.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     3.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     3.6      fun mk_all ((s, T), (P,n)) =
     3.7 -      if 0 mem loose_bnos P then
     3.8 +      if member (op =) (loose_bnos P) 0 then
     3.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    3.10        else (incr_boundvars ~1 P, n-1)
    3.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu May 06 08:43:51 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu May 06 08:44:19 2010 +0200
     4.3 @@ -51,7 +51,7 @@
     4.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     4.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     4.6      fun mk_all ((s, T), (P,n)) =
     4.7 -      if 0 mem loose_bnos P then
     4.8 +      if member (op =) (loose_bnos P) 0 then
     4.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    4.10        else (incr_boundvars ~1 P, n-1)
    4.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu May 06 08:43:51 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu May 06 08:44:19 2010 +0200
     5.3 @@ -66,7 +66,7 @@
     5.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     5.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     5.6      fun mk_all ((s, T), (P,n)) =
     5.7 -      if 0 mem loose_bnos P then
     5.8 +      if member (op =) (loose_bnos P) 0 then
     5.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    5.10        else (incr_boundvars ~1 P, n-1)
    5.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     6.1 --- a/src/HOL/HOL.thy	Thu May 06 08:43:51 2010 +0200
     6.2 +++ b/src/HOL/HOL.thy	Thu May 06 08:44:19 2010 +0200
     6.3 @@ -1963,7 +1963,7 @@
     6.4  
     6.5  text {* Avoid some named infixes in evaluation environment *}
     6.6  
     6.7 -code_reserved Eval oo ooo oooo upto downto orf andf mem mem_int mem_string
     6.8 +code_reserved Eval oo ooo oooo upto downto orf andf
     6.9  
    6.10  setup {*
    6.11    Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
     7.1 --- a/src/HOL/Import/hol4rews.ML	Thu May 06 08:43:51 2010 +0200
     7.2 +++ b/src/HOL/Import/hol4rews.ML	Thu May 06 08:44:19 2010 +0200
     7.3 @@ -604,9 +604,9 @@
     7.4                  val defname = Thm.def_name name
     7.5                  val pdefname = name ^ "_primdef"
     7.6              in
     7.7 -                if not (defname mem used)
     7.8 +                if not (member (op =) used defname)
     7.9                  then F defname                 (* name_def *)
    7.10 -                else if not (pdefname mem used)
    7.11 +                else if not (member (op =) used pdefname)
    7.12                  then F pdefname                (* name_primdef *)
    7.13                  else F (Name.variant used pdefname) (* last resort *)
    7.14              end
     8.1 --- a/src/HOL/Import/proof_kernel.ML	Thu May 06 08:43:51 2010 +0200
     8.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu May 06 08:44:19 2010 +0200
     8.3 @@ -276,6 +276,7 @@
     8.4      in
     8.5          F
     8.6      end
     8.7 +infix mem;
     8.8  fun i mem L =
     8.9      let fun itr [] = false
    8.10            | itr (a::rst) = i=a orelse itr rst
    8.11 @@ -1091,7 +1092,7 @@
    8.12      let
    8.13          fun F vars (Bound _) = vars
    8.14            | F vars (tm as Free _) =
    8.15 -            if tm mem vars
    8.16 +            if member (op =) vars tm
    8.17              then vars
    8.18              else (tm::vars)
    8.19            | F vars (Const _) = vars
     9.1 --- a/src/HOL/Import/shuffler.ML	Thu May 06 08:43:51 2010 +0200
     9.2 +++ b/src/HOL/Import/shuffler.ML	Thu May 06 08:44:19 2010 +0200
     9.3 @@ -550,7 +550,7 @@
     9.4  fun match_consts ignore t (* th *) =
     9.5      let
     9.6          fun add_consts (Const (c, _), cs) =
     9.7 -            if c mem_string ignore
     9.8 +            if member (op =) ignore c
     9.9              then cs
    9.10              else insert (op =) c cs
    9.11            | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    10.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu May 06 08:43:51 2010 +0200
    10.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu May 06 08:44:19 2010 +0200
    10.3 @@ -528,8 +528,8 @@
    10.4     end
    10.5   end;
    10.6  
    10.7 -fun isspace x = x = " " ;
    10.8 -fun isnum x = x mem_string ["0","1","2","3","4","5","6","7","8","9"]
    10.9 +fun isspace x = (x = " ");
   10.10 +fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x;
   10.11  
   10.12  (* More parser basics.                                                       *)
   10.13  
    11.1 --- a/src/HOL/Library/normarith.ML	Thu May 06 08:43:51 2010 +0200
    11.2 +++ b/src/HOL/Library/normarith.ML	Thu May 06 08:44:19 2010 +0200
    11.3 @@ -311,7 +311,7 @@
    11.4          in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
    11.5          end
    11.6         val goodverts = filter check_solution rawverts
    11.7 -       val signfixups = map (fn n => if n mem_int  f then ~1 else 1) nvs 
    11.8 +       val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs 
    11.9        in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts
   11.10        end
   11.11       val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] 
    12.1 --- a/src/HOL/Library/reflection.ML	Thu May 06 08:43:51 2010 +0200
    12.2 +++ b/src/HOL/Library/reflection.ML	Thu May 06 08:44:19 2010 +0200
    12.3 @@ -149,7 +149,7 @@
    12.4                Pattern.match thy
    12.5                  ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    12.6                  (Vartab.empty, Vartab.empty)
    12.7 -            val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
    12.8 +            val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
    12.9              val (fts,its) =
   12.10                (map (snd o snd) fnvs,
   12.11                 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    13.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 06 08:43:51 2010 +0200
    13.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 06 08:44:19 2010 +0200
    13.3 @@ -921,7 +921,7 @@
    13.4  check_finity gl bl ((t,cl)::r) b =
    13.5  let
    13.6  fun listmem [] _ = true |
    13.7 -listmem (a::r) l = if (a mem l) then (listmem r l) else false;
    13.8 +listmem (a::r) l = if member (op =) l a then (listmem r l) else false;
    13.9  fun snd_listmem [] _ = true |
   13.10  snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false;
   13.11  in
   13.12 @@ -966,7 +966,7 @@
   13.13   (ll @ (new_types r))
   13.14  end;
   13.15  in
   13.16 -        if (a mem done)
   13.17 +        if member (op =) done a
   13.18          then (preprocess_td sg b done)
   13.19          else
   13.20          (let
    14.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Thu May 06 08:43:51 2010 +0200
    14.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Thu May 06 08:44:19 2010 +0200
    14.3 @@ -361,7 +361,7 @@
    14.4     val t' = canonize_term t comms;
    14.5     val u' = canonize_term u comms;
    14.6   in 
    14.7 -   if s mem comms andalso Term_Ord.termless (u', t')
    14.8 +   if member (op =) comms s andalso Term_Ord.termless (u', t')
    14.9     then Const (s, T) $ u' $ t'
   14.10     else Const (s, T) $ t' $ u'
   14.11   end
    15.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu May 06 08:43:51 2010 +0200
    15.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu May 06 08:44:19 2010 +0200
    15.3 @@ -218,8 +218,8 @@
    15.4  
    15.5  fun is_forbidden_theorem (s, th) =
    15.6    let val consts = Term.add_const_names (prop_of th) [] in
    15.7 -    exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
    15.8 -    exists (fn s' => s' mem forbidden_consts) consts orelse
    15.9 +    exists (member (op =) (space_explode "." s)) forbidden_thms orelse
   15.10 +    exists (member (op =) forbidden_consts) consts orelse
   15.11      length (space_explode "." s) <> 2 orelse
   15.12      String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
   15.13      String.isSuffix "_def" s orelse
    16.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu May 06 08:43:51 2010 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu May 06 08:44:19 2010 +0200
    16.3 @@ -66,7 +66,7 @@
    16.4  
    16.5  fun mk_case_names_exhausts descr new =
    16.6    map (Rule_Cases.case_names o exhaust_cases descr o #1)
    16.7 -    (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    16.8 +    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
    16.9  
   16.10  end;
   16.11  
   16.12 @@ -131,7 +131,7 @@
   16.13        let
   16.14          val (aT as Type (a, []), S) = dest_permT T;
   16.15          val (bT as Type (b, []), _) = dest_permT U
   16.16 -      in if aT mem permTs_of u andalso aT <> bT then
   16.17 +      in if member (op =) (permTs_of u) aT andalso aT <> bT then
   16.18            let
   16.19              val cp = cp_inst_of thy a b;
   16.20              val dj = dj_thm_of thy b a;
   16.21 @@ -1772,7 +1772,7 @@
   16.22                      val params' = params1 @ params2;
   16.23                      val rec_prems = filter (fn th => case prop_of th of
   16.24                          _ $ p => (case head_of p of
   16.25 -                          Const (s, _) => s mem rec_set_names
   16.26 +                          Const (s, _) => member (op =) rec_set_names s
   16.27                          | _ => false)
   16.28                        | _ => false) prems';
   16.29                      val fresh_prems = filter (fn th => case prop_of th of
    17.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu May 06 08:43:51 2010 +0200
    17.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu May 06 08:44:19 2010 +0200
    17.3 @@ -43,7 +43,7 @@
    17.4  fun mk_perm_bool_simproc names = Simplifier.simproc_i
    17.5    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
    17.6      fn Const ("Nominal.perm", _) $ _ $ t =>
    17.7 -         if the_default "" (try (head_of #> dest_Const #> fst) t) mem names
    17.8 +         if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    17.9           then SOME perm_bool else NONE
   17.10       | _ => NONE);
   17.11  
   17.12 @@ -73,7 +73,7 @@
   17.13  
   17.14  fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
   17.15        Const (name, _) =>
   17.16 -        if name mem names then SOME (f p q) else NONE
   17.17 +        if member (op =) names name then SOME (f p q) else NONE
   17.18      | _ => NONE)
   17.19    | split_conj _ _ _ _ = NONE;
   17.20  
   17.21 @@ -92,7 +92,7 @@
   17.22  fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
   17.23        (case head_of p of
   17.24           Const (name, _) =>
   17.25 -           if name mem names then SOME (HOLogic.mk_conj (p,
   17.26 +           if member (op =) names name then SOME (HOLogic.mk_conj (p,
   17.27               Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
   17.28                 (subst_bounds (pis, strip_all pis q))))
   17.29             else NONE
   17.30 @@ -214,7 +214,7 @@
   17.31      fun lift_prem (t as (f $ u)) =
   17.32            let val (p, ts) = strip_comb t
   17.33            in
   17.34 -            if p mem ps then
   17.35 +            if member (op =) ps p then
   17.36                Const (inductive_forall_name,
   17.37                  (fsT --> HOLogic.boolT) --> HOLogic.boolT) $
   17.38                    Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
   17.39 @@ -510,7 +510,7 @@
   17.40                    val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis);
   17.41                    val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
   17.42                       (fn x as Free _ =>
   17.43 -                           if x mem args then x
   17.44 +                           if member (op =) args x then x
   17.45                             else (case AList.lookup op = tab x of
   17.46                               SOME y => y
   17.47                             | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)
    18.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu May 06 08:43:51 2010 +0200
    18.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu May 06 08:44:19 2010 +0200
    18.3 @@ -46,7 +46,7 @@
    18.4  fun mk_perm_bool_simproc names = Simplifier.simproc_i
    18.5    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
    18.6      fn Const ("Nominal.perm", _) $ _ $ t =>
    18.7 -         if the_default "" (try (head_of #> dest_Const #> fst) t) mem names
    18.8 +         if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    18.9           then SOME perm_bool else NONE
   18.10       | _ => NONE);
   18.11  
   18.12 @@ -77,7 +77,7 @@
   18.13  
   18.14  fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
   18.15        Const (name, _) =>
   18.16 -        if name mem names then SOME (f p q) else NONE
   18.17 +        if member (op =) names name then SOME (f p q) else NONE
   18.18      | _ => NONE)
   18.19    | split_conj _ _ _ _ = NONE;
   18.20  
   18.21 @@ -96,7 +96,7 @@
   18.22  fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
   18.23        (case head_of p of
   18.24           Const (name, _) =>
   18.25 -           if name mem names then SOME (HOLogic.mk_conj (p,
   18.26 +           if member (op =) names name then SOME (HOLogic.mk_conj (p,
   18.27               Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
   18.28                 (subst_bounds (pis, strip_all pis q))))
   18.29             else NONE
   18.30 @@ -239,7 +239,7 @@
   18.31      fun lift_prem (t as (f $ u)) =
   18.32            let val (p, ts) = strip_comb t
   18.33            in
   18.34 -            if p mem ps then
   18.35 +            if member (op =) ps p then
   18.36                Const (inductive_forall_name,
   18.37                  (fsT --> HOLogic.boolT) --> HOLogic.boolT) $
   18.38                    Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
    19.1 --- a/src/HOL/Statespace/state_space.ML	Thu May 06 08:43:51 2010 +0200
    19.2 +++ b/src/HOL/Statespace/state_space.ML	Thu May 06 08:44:19 2010 +0200
    19.3 @@ -528,7 +528,7 @@
    19.4              | dups => ["Duplicate renaming(s) for " ^ commas dups])
    19.5  
    19.6          val cnames = map fst components;
    19.7 -        val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of
    19.8 +        val err_rename_unknowns = (case subtract (op =) cnames rnames of
    19.9                [] => []
   19.10               | rs => ["Unknown components " ^ commas rs]);
   19.11  
    20.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu May 06 08:43:51 2010 +0200
    20.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu May 06 08:44:19 2010 +0200
    20.3 @@ -309,7 +309,7 @@
    20.4              val T' = typ_of_dtyp descr' sorts dt;
    20.5              val (Us, U) = strip_type T'
    20.6            in (case strip_dtyp dt of
    20.7 -              (_, DtRec j) => if j mem ks' then
    20.8 +              (_, DtRec j) => if member (op =) ks' j then
    20.9                    (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
   20.10                       (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
   20.11                     Ts @ [Us ---> Univ_elT])
    21.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu May 06 08:43:51 2010 +0200
    21.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu May 06 08:44:19 2010 +0200
    21.3 @@ -136,7 +136,7 @@
    21.4      val getP = if can HOLogic.dest_imp (hd ts) then
    21.5        (apfst SOME) o HOLogic.dest_imp else pair NONE;
    21.6      val flt = if null indnames then I else
    21.7 -      filter (fn Free (s, _) => s mem indnames | _ => false);
    21.8 +      filter (fn Free (s, _) => member (op =) indnames s | _ => false);
    21.9      fun abstr (t1, t2) = (case t1 of
   21.10          NONE => (case flt (OldTerm.term_frees t2) of
   21.11              [Free (s, T)] => SOME (absfree (s, T, t2))
   21.12 @@ -300,7 +300,7 @@
   21.13      fun is_nonempty_dt is i =
   21.14        let
   21.15          val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
   21.16 -        fun arg_nonempty (_, DtRec i) = if i mem is then false
   21.17 +        fun arg_nonempty (_, DtRec i) = if member (op =) is i then false
   21.18                else is_nonempty_dt (i::is) i
   21.19            | arg_nonempty _ = true;
   21.20        in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
    22.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu May 06 08:43:51 2010 +0200
    22.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu May 06 08:44:19 2010 +0200
    22.3 @@ -306,11 +306,11 @@
    22.4             map_node node_id (K (NONE, module',
    22.5               string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
    22.6                 [str ";"])) ^ "\n\n" ^
    22.7 -             (if "term_of" mem !mode then
    22.8 +             (if member (op =) (!mode) "term_of" then
    22.9                  string_of (Pretty.blk (0, separate Pretty.fbrk
   22.10                    (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   22.11                else "") ^
   22.12 -             (if "test" mem !mode then
   22.13 +             (if member (op =) (!mode) "test" then
   22.14                  string_of (Pretty.blk (0, separate Pretty.fbrk
   22.15                    (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   22.16                else ""))) gr2
    23.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu May 06 08:43:51 2010 +0200
    23.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu May 06 08:44:19 2010 +0200
    23.3 @@ -41,16 +41,16 @@
    23.4        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    23.5  
    23.6      val rec_result_Ts = map (fn ((i, _), P) =>
    23.7 -      if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
    23.8 +      if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
    23.9          (descr ~~ pnames);
   23.10  
   23.11      fun make_pred i T U r x =
   23.12 -      if i mem is then
   23.13 +      if member (op =) is i then
   23.14          Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x
   23.15        else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x;
   23.16  
   23.17      fun mk_all i s T t =
   23.18 -      if i mem is then list_all_free ([(s, T)], t) else t;
   23.19 +      if member (op =) is i then list_all_free ([(s, T)], t) else t;
   23.20  
   23.21      val (prems, rec_fns) = split_list (flat (fst (fold_map
   23.22        (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
   23.23 @@ -66,7 +66,7 @@
   23.24                    val vs' = filter_out is_unit vs;
   23.25                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
   23.26                    val f' = Envir.eta_contract (list_abs_free
   23.27 -                    (map dest_Free vs, if i mem is then list_comb (f, vs')
   23.28 +                    (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
   23.29                        else HOLogic.unit));
   23.30                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
   23.31                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
   23.32 @@ -100,7 +100,7 @@
   23.33          (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
   23.34      val r = if null is then Extraction.nullt else
   23.35        foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
   23.36 -        if i mem is then SOME
   23.37 +        if member (op =) is i then SOME
   23.38            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
   23.39          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
   23.40      val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
   23.41 @@ -131,7 +131,7 @@
   23.42      val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
   23.43      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
   23.44      val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
   23.45 -      tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs);
   23.46 +      member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
   23.47      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
   23.48  
   23.49      val prf =
    24.1 --- a/src/HOL/Tools/Function/function_common.ML	Thu May 06 08:43:51 2010 +0200
    24.2 +++ b/src/HOL/Tools/Function/function_common.ML	Thu May 06 08:44:19 2010 +0200
    24.3 @@ -244,7 +244,7 @@
    24.4  
    24.5          val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
    24.6  
    24.7 -        val _ = fname mem fnames
    24.8 +        val _ = member (op =) fnames fname 
    24.9            orelse input_error ("Head symbol of left hand side must be " ^
   24.10              plural "" "one out of " fnames ^ commas_quote fnames)
   24.11  
   24.12 @@ -259,7 +259,7 @@
   24.13             " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   24.14  
   24.15          val _ = forall (not o Term.exists_subterm
   24.16 -          (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
   24.17 +          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
   24.18            orelse input_error "Defined function may not occur in premises or arguments"
   24.19  
   24.20          val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
    25.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 06 08:43:51 2010 +0200
    25.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 06 08:44:19 2010 +0200
    25.3 @@ -2178,7 +2178,7 @@
    25.4        val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
    25.5        val (c, _) = strip_comb t
    25.6        in (case c of
    25.7 -        Const (name, _) => name mem_string constr_consts
    25.8 +        Const (name, _) => member (op =) constr_consts name
    25.9          | _ => false) end))
   25.10    else false
   25.11  
    26.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu May 06 08:43:51 2010 +0200
    26.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu May 06 08:44:19 2010 +0200
    26.3 @@ -538,6 +538,8 @@
    26.4  
    26.5  open Generated_Cooper;
    26.6  
    26.7 +fun member eq = Library.member eq;
    26.8 +
    26.9  fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
   26.10  fun i_of_term vs t = case t
   26.11   of Free (xn, xT) => (case AList.lookup (op aconv) vs t
   26.12 @@ -593,12 +595,12 @@
   26.13  in
   26.14  fun term_bools acc t =
   26.15  case t of
   26.16 -    (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
   26.17 +    (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
   26.18              else insert (op aconv) t acc
   26.19 -  | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
   26.20 +  | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
   26.21              else insert (op aconv) t acc
   26.22    | Abs p => term_bools acc (snd (variant_abs p))
   26.23 -  | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
   26.24 +  | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
   26.25  end;
   26.26  
   26.27  fun myassoc2 l v =
    27.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 08:43:51 2010 +0200
    27.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 08:44:19 2010 +0200
    27.3 @@ -67,9 +67,9 @@
    27.4   | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
    27.5  
    27.6   fun ty cts t = 
    27.7 - if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false 
    27.8 + if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
    27.9      else case term_of t of 
   27.10 -      c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
   27.11 +      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
   27.12                 then not (isnum l orelse isnum r)
   27.13                 else not (member (op aconv) cts c)
   27.14      | c$_ => not (member (op aconv) cts c)
   27.15 @@ -85,8 +85,8 @@
   27.16  in 
   27.17  fun is_relevant ctxt ct = 
   27.18   subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
   27.19 - andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
   27.20 - andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
   27.21 + andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
   27.22 + andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
   27.23  
   27.24  fun int_nat_terms ctxt ct =
   27.25   let 
    28.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu May 06 08:43:51 2010 +0200
    28.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu May 06 08:44:19 2010 +0200
    28.3 @@ -728,7 +728,7 @@
    28.4    val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
    28.5    val ty_substs =
    28.6      if qtys = [] then all_ty_substs else
    28.7 -    filter (fn (_, qty) => qty mem qtys) all_ty_substs
    28.8 +    filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs
    28.9    val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
   28.10    fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
   28.11    val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
    29.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu May 06 08:43:51 2010 +0200
    29.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu May 06 08:44:19 2010 +0200
    29.3 @@ -387,7 +387,7 @@
    29.4  
    29.5  (*Ignore blacklisted basenames*)
    29.6  fun add_multi_names (a, ths) pairs =
    29.7 -  if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
    29.8 +  if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
    29.9    else add_single_names (a, ths) pairs;
   29.10  
   29.11  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    30.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu May 06 08:43:51 2010 +0200
    30.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu May 06 08:44:19 2010 +0200
    30.3 @@ -410,7 +410,7 @@
    30.4    | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
    30.5        arity_clause dfg seen n (tcons,ars)
    30.6    | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
    30.7 -      if class mem_string seen then (*multiple arities for the same tycon, class pair*)
    30.8 +      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
    30.9            make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   30.10            arity_clause dfg seen (n+1) (tcons,ars)
   30.11        else
    31.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu May 06 08:43:51 2010 +0200
    31.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu May 06 08:44:19 2010 +0200
    31.3 @@ -76,7 +76,7 @@
    31.4    let val slist = Unsynchronized.ref names
    31.5        val vname = Unsynchronized.ref "u"
    31.6        fun new() =
    31.7 -         if !vname mem_string (!slist)
    31.8 +         if member (op =) (!slist) (!vname)
    31.9           then (vname := Symbol.bump_string (!vname);  new())
   31.10           else (slist := !vname :: !slist;  !vname)
   31.11    in
    32.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu May 06 08:43:51 2010 +0200
    32.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu May 06 08:44:19 2010 +0200
    32.3 @@ -122,7 +122,7 @@
    32.4  		  | dual x                      = HOLogic.Not $ x
    32.5  		(* Term.term list -> bool *)
    32.6  		fun has_duals []      = false
    32.7 -		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
    32.8 +		  | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
    32.9  	in
   32.10  		has_duals (HOLogic.disjuncts c)
   32.11  	end;
    33.1 --- a/src/HOL/Tools/hologic.ML	Thu May 06 08:43:51 2010 +0200
    33.2 +++ b/src/HOL/Tools/hologic.ML	Thu May 06 08:44:19 2010 +0200
    33.3 @@ -356,7 +356,7 @@
    33.4  fun mk_ptupleT ps =
    33.5    let
    33.6      fun mk p Ts =
    33.7 -      if p mem ps then
    33.8 +      if member (op =) ps p then
    33.9          let
   33.10            val (T, Ts') = mk (1::p) Ts;
   33.11            val (U, Ts'') = mk (2::p) Ts'
   33.12 @@ -366,7 +366,7 @@
   33.13  
   33.14  fun strip_ptupleT ps =
   33.15    let
   33.16 -    fun factors p T = if p mem ps then (case T of
   33.17 +    fun factors p T = if member (op =) ps p then (case T of
   33.18          Type ("*", [T1, T2]) =>
   33.19            factors (1::p) T1 @ factors (2::p) T2
   33.20        | _ => ptuple_err "strip_ptupleT") else [T]
   33.21 @@ -382,7 +382,7 @@
   33.22  fun mk_ptuple ps =
   33.23    let
   33.24      fun mk p T ts =
   33.25 -      if p mem ps then (case T of
   33.26 +      if member (op =) ps p then (case T of
   33.27            Type ("*", [T1, T2]) =>
   33.28              let
   33.29                val (t, ts') = mk (1::p) T1 ts;
   33.30 @@ -394,7 +394,7 @@
   33.31  
   33.32  fun strip_ptuple ps =
   33.33    let
   33.34 -    fun dest p t = if p mem ps then (case t of
   33.35 +    fun dest p t = if member (op =) ps p then (case t of
   33.36          Const ("Pair", _) $ t $ u =>
   33.37            dest (1::p) t @ dest (2::p) u
   33.38        | _ => ptuple_err "strip_ptuple") else [t]
   33.39 @@ -413,7 +413,7 @@
   33.40  fun mk_psplits ps T T3 u =
   33.41    let
   33.42      fun ap ((p, T) :: pTs) =
   33.43 -          if p mem ps then (case T of
   33.44 +          if member (op =) ps p then (case T of
   33.45                Type ("*", [T1, T2]) =>
   33.46                  split_const (T1, T2, map snd pTs ---> T3) $
   33.47                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
    34.1 --- a/src/HOL/Tools/inductive.ML	Thu May 06 08:43:51 2010 +0200
    34.2 +++ b/src/HOL/Tools/inductive.ML	Thu May 06 08:44:19 2010 +0200
    34.3 @@ -288,7 +288,7 @@
    34.4            then err bad_ind_occ else ();
    34.5  
    34.6      fun check_prem' prem t =
    34.7 -      if head_of t mem cs then
    34.8 +      if member (op =) cs (head_of t) then
    34.9          check_ind (err_in_prem ctxt err_name rule prem) t
   34.10        else (case t of
   34.11            Abs (_, _, t) => check_prem' prem t
   34.12 @@ -301,7 +301,7 @@
   34.13    in
   34.14      (case concl of
   34.15         Const (@{const_name Trueprop}, _) $ t =>
   34.16 -         if head_of t mem cs then
   34.17 +         if member (op =) cs (head_of t) then
   34.18             (check_ind (err_in_rule ctxt err_name rule') t;
   34.19              List.app check_prem (prems ~~ aprems))
   34.20           else err_in_rule ctxt err_name rule' bad_concl
    35.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu May 06 08:43:51 2010 +0200
    35.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu May 06 08:44:19 2010 +0200
    35.3 @@ -140,7 +140,7 @@
    35.4    fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm [];
    35.5  
    35.6  fun get_args _ _ [] = ([], [])
    35.7 -  | get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x)
    35.8 +  | get_args is i (x::xs) = (if member (op =) is i then apfst else apsnd) (cons x)
    35.9        (get_args is (i+1) xs);
   35.10  
   35.11  fun merge xs [] = xs
   35.12 @@ -237,7 +237,7 @@
   35.13              end)
   35.14                ps));
   35.15  
   35.16 -fun use_random () = "random_ind" mem !Codegen.mode;
   35.17 +fun use_random () = member (op =) (!Codegen.mode) "random_ind";
   35.18  
   35.19  fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
   35.20    let
   35.21 @@ -557,7 +557,7 @@
   35.22  
   35.23  fun mk_extra_defs thy defs gr dep names module ts =
   35.24    fold (fn name => fn gr =>
   35.25 -    if name mem names then gr
   35.26 +    if member (op =) names name then gr
   35.27      else
   35.28        (case get_clauses thy name of
   35.29          NONE => gr
   35.30 @@ -576,7 +576,7 @@
   35.31        val args = List.take (snd (strip_comb u), nparms);
   35.32        val arg_vs = maps term_vs args;
   35.33  
   35.34 -      fun get_nparms s = if s mem names then SOME nparms else
   35.35 +      fun get_nparms s = if member (op =) names s then SOME nparms else
   35.36          Option.map #3 (get_clauses thy s);
   35.37  
   35.38        fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
   35.39 @@ -585,7 +585,7 @@
   35.40              Prem ([t, u], eq, false)
   35.41          | dest_prem (_ $ t) =
   35.42              (case strip_comb t of
   35.43 -              (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
   35.44 +              (v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t
   35.45              | (c as Const (s, _), ts) =>
   35.46                  (case get_nparms s of
   35.47                    NONE => Sidecond t
   35.48 @@ -704,7 +704,7 @@
   35.49      val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
   35.50      val xs' = map (fn Bound i => nth xs (k - i)) ts;
   35.51      fun conv xs js =
   35.52 -      if js mem fs then
   35.53 +      if member (op =) fs js then
   35.54          let
   35.55            val (p, xs') = conv xs (1::js);
   35.56            val (q, xs'') = conv xs' (2::js)
    36.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu May 06 08:43:51 2010 +0200
    36.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu May 06 08:44:19 2010 +0200
    36.3 @@ -57,7 +57,7 @@
    36.4  
    36.5  fun relevant_vars prop = List.foldr (fn
    36.6        (Var ((a, i), T), vs) => (case strip_type T of
    36.7 -        (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs
    36.8 +        (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
    36.9        | _ => vs)
   36.10      | (_, vs) => vs) [] (OldTerm.term_vars prop);
   36.11  
   36.12 @@ -90,7 +90,7 @@
   36.13            val xs = map (pair "x") Ts;
   36.14            val u = list_comb (t, map Bound (i - 1 downto 0))
   36.15          in 
   36.16 -          if a mem vs then
   36.17 +          if member (op =) vs a then
   36.18              list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
   36.19            else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
   36.20          end
   36.21 @@ -257,7 +257,7 @@
   36.22    let
   36.23      val rvs = map fst (relevant_vars (prop_of rule));
   36.24      val xs = rev (Term.add_vars (prop_of rule) []);
   36.25 -    val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
   36.26 +    val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
   36.27      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
   36.28      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
   36.29      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
   36.30 @@ -292,7 +292,7 @@
   36.31        Sign.root_path |>
   36.32        Sign.add_path (Long_Name.implode prfx);
   36.33      val (ty_eqs, rlz_eqs) = split_list
   36.34 -      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
   36.35 +      (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss);
   36.36  
   36.37      val thy1' = thy1 |>
   36.38        Theory.copy |>
   36.39 @@ -300,7 +300,7 @@
   36.40        fold (fn s => AxClass.axiomatize_arity
   36.41          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   36.42          Extraction.add_typeof_eqns_i ty_eqs;
   36.43 -    val dts = map_filter (fn (s, rs) => if s mem rsets then
   36.44 +    val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
   36.45        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   36.46  
   36.47      (** datatype representing computational content of inductive set **)
   36.48 @@ -363,7 +363,7 @@
   36.49  
   36.50      (** realizer for induction rule **)
   36.51  
   36.52 -    val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
   36.53 +    val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then
   36.54        SOME (fst (fst (dest_Var (head_of P)))) else NONE)
   36.55          (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
   36.56  
   36.57 @@ -471,7 +471,7 @@
   36.58              list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
   36.59                (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
   36.60      val elimps = map_filter (fn ((s, intrs), p) =>
   36.61 -      if s mem rsets then SOME (p, intrs) else NONE)
   36.62 +      if member (op =) rsets s then SOME (p, intrs) else NONE)
   36.63          (rss' ~~ (elims ~~ #elims ind_info));
   36.64      val thy6 =
   36.65        fold (fn p as (((((elim, _), _), _), _), _) =>
    37.1 --- a/src/HOL/Tools/inductive_set.ML	Thu May 06 08:43:51 2010 +0200
    37.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu May 06 08:44:19 2010 +0200
    37.3 @@ -419,7 +419,7 @@
    37.4        | infer (t $ u) = infer t #> infer u
    37.5        | infer _ = I;
    37.6      val new_arities = filter_out
    37.7 -      (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
    37.8 +      (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 1
    37.9          | _ => false) (fold (snd #> infer) intros []);
   37.10      val params' = map (fn x =>
   37.11        (case AList.lookup op = new_arities x of
    38.1 --- a/src/HOL/Tools/lin_arith.ML	Thu May 06 08:43:51 2010 +0200
    38.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu May 06 08:44:19 2010 +0200
    38.3 @@ -221,7 +221,7 @@
    38.4          in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
    38.5          handle TERM _ => add_atom all m pi)
    38.6      | poly (all as Const f $ x, m, pi) =
    38.7 -        if f mem inj_consts then poly (x, m, pi) else add_atom all m pi
    38.8 +        if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
    38.9      | poly (all, m, pi) =
   38.10          add_atom all m pi
   38.11    val (p, i) = poly (lhs, Rat.one, ([], Rat.zero))
    39.1 --- a/src/HOL/Tools/old_primrec.ML	Thu May 06 08:43:51 2010 +0200
    39.2 +++ b/src/HOL/Tools/old_primrec.ML	Thu May 06 08:44:19 2010 +0200
    39.3 @@ -120,7 +120,7 @@
    39.4            let
    39.5              val (f, ts) = strip_comb t;
    39.6            in
    39.7 -            if is_Const f andalso dest_Const f mem map fst rec_eqns then
    39.8 +            if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then
    39.9                let
   39.10                  val fnameT' as (fname', _) = dest_Const f;
   39.11                  val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
    40.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu May 06 08:43:51 2010 +0200
    40.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu May 06 08:44:19 2010 +0200
    40.3 @@ -114,7 +114,7 @@
    40.4           in (case xs of
    40.5               [_] => (module, put_code module fundef gr2)
    40.6             | _ =>
    40.7 -             if not (dep mem xs) then
    40.8 +             if not (member (op =) xs dep) then
    40.9                 let
   40.10                   val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   40.11                   val module' = if_library thyname module;
    41.1 --- a/src/HOL/Tools/refute.ML	Thu May 06 08:43:51 2010 +0200
    41.2 +++ b/src/HOL/Tools/refute.ML	Thu May 06 08:44:19 2010 +0200
    41.3 @@ -463,7 +463,7 @@
    41.4    in
    41.5      (* I'm not quite sure if checking the name 's' is sufficient, *)
    41.6      (* or if we should also check the type 'T'.                   *)
    41.7 -    s mem_string class_const_names
    41.8 +    member (op =) class_const_names s
    41.9    end;
   41.10  
   41.11  (* ------------------------------------------------------------------------- *)
   41.12 @@ -499,7 +499,7 @@
   41.13    in
   41.14      (* I'm not quite sure if checking the name 's' is sufficient, *)
   41.15      (* or if we should also check the type 'T'.                   *)
   41.16 -    s mem_string rec_names
   41.17 +    member (op =) rec_names s
   41.18    end;
   41.19  
   41.20  (* ------------------------------------------------------------------------- *)
   41.21 @@ -932,7 +932,7 @@
   41.22                | Datatype_Aux.DtType (_, ds) =>
   41.23                  collect_types dT (fold_rev collect_dtyp ds acc)
   41.24                | Datatype_Aux.DtRec i =>
   41.25 -                if dT mem acc then
   41.26 +                if member (op =) acc dT then
   41.27                    acc  (* prevent infinite recursion *)
   41.28                  else
   41.29                    let
   41.30 @@ -2248,7 +2248,7 @@
   41.31                            (* if 't_elem' existed at the previous depth,    *)
   41.32                            (* proceed recursively, otherwise map the entire *)
   41.33                            (* subtree to "undefined"                        *)
   41.34 -                          if t_elem mem terms' then
   41.35 +                          if member (op =) terms' t_elem then
   41.36                              make_constr ds off
   41.37                            else
   41.38                              (make_undef ds, off))
    42.1 --- a/src/HOL/Tools/sat_solver.ML	Thu May 06 08:43:51 2010 +0200
    42.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu May 06 08:44:19 2010 +0200
    42.3 @@ -350,7 +350,7 @@
    42.4      o (map (map literal_from_int))
    42.5      o clauses
    42.6      o (map int_from_string)
    42.7 -    o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"])))
    42.8 +    o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"])))
    42.9      o filter_preamble
   42.10      o filter (fn l => l <> "")
   42.11      o split_lines
   42.12 @@ -421,7 +421,7 @@
   42.13          SOME (y::x::xs)
   42.14      (* int list -> int -> bool *)
   42.15      fun assignment_from_list xs i =
   42.16 -      i mem xs
   42.17 +      member (op =) xs i
   42.18      (* int list -> SatSolver.result *)
   42.19      fun solver_loop xs =
   42.20        if PropLogic.eval (assignment_from_list xs) fm then
   42.21 @@ -490,7 +490,7 @@
   42.22        end
   42.23        (* int list -> int option *)
   42.24        fun fresh_var xs =
   42.25 -        Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices
   42.26 +        find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
   42.27        (* int list -> prop_formula -> int list option *)
   42.28        (* partial assignment 'xs' *)
   42.29        fun dpll xs fm =
    43.1 --- a/src/HOL/Tools/typedef_codegen.ML	Thu May 06 08:43:51 2010 +0200
    43.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Thu May 06 08:44:19 2010 +0200
    43.3 @@ -78,7 +78,7 @@
    43.4                        Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
    43.5                          Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    43.6                          Codegen.str "x) = x;"]) ^ "\n\n" ^
    43.7 -                      (if "term_of" mem !Codegen.mode then
    43.8 +                      (if member (op =) (!Codegen.mode) "term_of" then
    43.9                          Codegen.string_of (Pretty.block [Codegen.str "fun ",
   43.10                            Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
   43.11                            Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
   43.12 @@ -89,7 +89,7 @@
   43.13                            Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
   43.14                            Codegen.str "x;"]) ^ "\n\n"
   43.15                         else "") ^
   43.16 -                      (if "test" mem !Codegen.mode then
   43.17 +                      (if member (op =) (!Codegen.mode) "test" then
   43.18                          Codegen.string_of (Pretty.block [Codegen.str "fun ",
   43.19                            Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
   43.20                            Codegen.str "i =", Pretty.brk 1,
    44.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Thu May 06 08:43:51 2010 +0200
    44.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Thu May 06 08:44:19 2010 +0200
    44.3 @@ -16,7 +16,7 @@
    44.4    let fun check_s(s,unchecked,checked) =
    44.5          let fun check_sa a unchecked =
    44.6                let fun check_sas t unchecked =
    44.7 -                    (if a mem extacts then
    44.8 +                    (if member (op =) extacts a then
    44.9                            (if transA(hom s,a,hom t) then ( )
   44.10                             else (writeln("Error: Mapping of Externals!");
   44.11                                   string_of_s s; writeln"";
   44.12 @@ -27,11 +27,11 @@
   44.13                                   string_of_s s; writeln"";
   44.14                                   string_of_a a; writeln"";
   44.15                                   string_of_s t;writeln"";writeln"" ));
   44.16 -                     if t mem checked then unchecked else insert (op =) t unchecked)
   44.17 +                     if member (op =) checked t then unchecked else insert (op =) t unchecked)
   44.18                in fold check_sas (nexts s a) unchecked end;
   44.19                val unchecked' = fold check_sa (extacts @ intacts) unchecked
   44.20 -        in    (if s mem startsI then 
   44.21 -                    (if hom(s) mem startsS then ()
   44.22 +        in    (if member (op =) startsI s then 
   44.23 +                    (if member (op =) startsS (hom s) then ()
   44.24                       else writeln("Error: At start states!"))
   44.25                 else ();  
   44.26                 checks(unchecked',s::checked)) end
    45.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 06 08:43:51 2010 +0200
    45.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 06 08:44:19 2010 +0200
    45.3 @@ -211,11 +211,11 @@
    45.4  
    45.5  (* used by write_alts *)
    45.6  fun write_alt thy (chead,tr) inp out int [] =
    45.7 -if (chead mem inp) then
    45.8 +if member (op =) inp chead then
    45.9  (
   45.10  error("Input action " ^ tr ^ " was not specified")
   45.11  ) else (
   45.12 -if (chead mem (out@int)) then
   45.13 +if member (op =) out chead orelse member (op =) int chead then
   45.14  (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   45.15  (tr ^ " => False",tr ^ " => False")) |
   45.16  write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   45.17 @@ -227,9 +227,9 @@
   45.18  occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
   45.19  in
   45.20  if (chead=(hd_of a)) then 
   45.21 -(if ((chead mem inp) andalso e) then (
   45.22 +(if member (op =) inp chead andalso e then (
   45.23  error("Input action " ^ b ^ " has a precondition")
   45.24 -) else (if (chead mem (inp@out@int)) then 
   45.25 +) else (if member (op =) (inp@out@int) chead then 
   45.26      (if (occurs_again chead r) then (
   45.27  error("Two specifications for action: " ^ b)
   45.28      ) else (b ^ " => " ^ c,b ^ " => " ^ d))
   45.29 @@ -275,7 +275,7 @@
   45.30  check_free_primed _ = [];
   45.31  
   45.32  fun overlap [] _ = true |
   45.33 -overlap (a::r) l = if (a mem l) then (
   45.34 +overlap (a::r) l = if member (op =) l a then (
   45.35  error("Two occurences of action " ^ a ^ " in automaton signature")
   45.36  ) else (overlap r l);
   45.37  
    46.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 06 08:43:51 2010 +0200
    46.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 06 08:44:19 2010 +0200
    46.3 @@ -228,7 +228,7 @@
    46.4  fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = 
    46.5      (case cont_eta_contract body  of
    46.6         body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => 
    46.7 -       if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
    46.8 +       if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f 
    46.9         else   Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
   46.10       | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body'))
   46.11    | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
    47.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu May 06 08:43:51 2010 +0200
    47.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu May 06 08:44:19 2010 +0200
    47.3 @@ -554,9 +554,9 @@
    47.4      (* test for finiteness of domain definitions *)
    47.5      local
    47.6        val types = [@{type_name ssum}, @{type_name sprod}];
    47.7 -      fun finite d T = if T mem absTs then d else finite' d T
    47.8 +      fun finite d T = if member (op =) absTs T then d else finite' d T
    47.9        and finite' d (Type (c, Ts)) =
   47.10 -          let val d' = d andalso c mem types;
   47.11 +          let val d' = d andalso member (op =) types c;
   47.12            in forall (finite d') Ts end
   47.13          | finite' d _ = true;
   47.14      in
    48.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu May 06 08:43:51 2010 +0200
    48.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu May 06 08:44:19 2010 +0200
    48.3 @@ -292,7 +292,7 @@
    48.4         it has a possibly indirectly recursive argument that isn't/is possibly 
    48.5         indirectly lazy *)
    48.6      fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
    48.7 -          is_rec arg andalso not(rec_of arg mem ns) andalso
    48.8 +          is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
    48.9            ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
   48.10              rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
   48.11                (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
    49.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Thu May 06 08:43:51 2010 +0200
    49.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Thu May 06 08:44:19 2010 +0200
    49.3 @@ -62,7 +62,7 @@
    49.4    let val ts = Data.dest_sum t;
    49.5        val dpq = Data.mk_binop Data.div_name pq
    49.6        val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
    49.7 -      val d = if d1 mem ts then d1 else d2
    49.8 +      val d = if member (op =) ts d1 then d1 else d2
    49.9        val m = Data.mk_binop Data.mod_name pq
   49.10    in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
   49.11  
    50.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu May 06 08:43:51 2010 +0200
    50.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu May 06 08:44:19 2010 +0200
    50.3 @@ -389,7 +389,7 @@
    50.4             |> sort (int_ord o pairself abs)
    50.5             |> hd
    50.6           val (eq as Lineq(_,_,ceq,_),othereqs) =
    50.7 -               extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
    50.8 +               extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs
    50.9           val v = find_index (fn v => v = c) ceq
   50.10           val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
   50.11                                       (othereqs @ noneqs)
    51.1 --- a/src/Provers/order.ML	Thu May 06 08:43:51 2010 +0200
    51.2 +++ b/src/Provers/order.ML	Thu May 06 08:44:19 2010 +0200
    51.3 @@ -871,8 +871,8 @@
    51.4        val vi = getIndex v ntc
    51.5  
    51.6    in
    51.7 -      if ui mem xreachable andalso vi mem xreachable andalso
    51.8 -         ui mem yreachable andalso vi mem yreachable then (
    51.9 +      if member (op =) xreachable ui andalso member (op =) xreachable vi andalso
   51.10 +         member (op =) yreachable ui andalso member (op =) yreachable vi then (
   51.11  
   51.12    (case e of (Less (_, _, _)) =>
   51.13         let
    52.1 --- a/src/Provers/trancl.ML	Thu May 06 08:43:51 2010 +0200
    52.2 +++ b/src/Provers/trancl.ML	Thu May 06 08:44:19 2010 +0200
    52.3 @@ -452,8 +452,8 @@
    52.4  
    52.5     fun processTranclEdges [] = raise Cannot
    52.6     |   processTranclEdges (e::es) =
    52.7 -          if (upper e) mem Vx andalso (lower e) mem Vx
    52.8 -          andalso (upper e) mem Vy andalso (lower e) mem Vy
    52.9 +          if member (op =) Vx (upper e) andalso member (op =) Vx (lower e)
   52.10 +          andalso member (op =) Vy (upper e) andalso member (op =) Vy (lower e)
   52.11            then (
   52.12  
   52.13  
    53.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Thu May 06 08:43:51 2010 +0200
    53.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Thu May 06 08:44:19 2010 +0200
    53.3 @@ -227,8 +227,8 @@
    53.4     (* We allow sending proper document markup too; we map it back to dostep   *)
    53.5     (* and strip out metainfo elements. Markup correctness isn't checked: this *)
    53.6     (* is a compatibility measure to make it easy for interfaces.              *)
    53.7 -   | x => if (x mem PgipMarkup.doc_markup_elements) then
    53.8 -              if (x mem PgipMarkup.doc_markup_elements_ignored) then
    53.9 +   | x => if member (op =) PgipMarkup.doc_markup_elements x then
   53.10 +              if member (op =) PgipMarkup.doc_markup_elements_ignored x then
   53.11                    raise NoAction
   53.12                else 
   53.13                    Dostep { text = xmltext data } (* could separate out Doitem too *)
    54.1 --- a/src/Pure/library.ML	Thu May 06 08:43:51 2010 +0200
    54.2 +++ b/src/Pure/library.ML	Thu May 06 08:44:19 2010 +0200
    54.3 @@ -11,7 +11,7 @@
    54.4  infix 2 ?
    54.5  infix 3 o oo ooo oooo
    54.6  infix 4 ~~ upto downto
    54.7 -infix orf andf mem mem_int mem_string
    54.8 +infix orf andf
    54.9  
   54.10  signature BASIC_LIBRARY =
   54.11  sig
   54.12 @@ -164,9 +164,6 @@
   54.13    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
   54.14    val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
   54.15    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   54.16 -  val mem: ''a * ''a list -> bool
   54.17 -  val mem_int: int * int list -> bool
   54.18 -  val mem_string: string * string list -> bool
   54.19    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   54.20    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   54.21    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   54.22 @@ -801,13 +798,6 @@
   54.23    else fold_rev (insert eq) ys xs;
   54.24  
   54.25  
   54.26 -(* old-style infixes *)
   54.27 -
   54.28 -fun x mem xs = member (op =) xs x;
   54.29 -fun (x: int) mem_int xs = member (op =) xs x;
   54.30 -fun (x: string) mem_string xs = member (op =) xs x;
   54.31 -
   54.32 -
   54.33  (* subset and set equality *)
   54.34  
   54.35  fun subset eq (xs, ys) = forall (member eq ys) xs;
    55.1 --- a/src/Tools/Metis/metis_env.ML	Thu May 06 08:43:51 2010 +0200
    55.2 +++ b/src/Tools/Metis/metis_env.ML	Thu May 06 08:44:19 2010 +0200
    55.3 @@ -1,5 +1,5 @@
    55.4  (* Metis-specific ML environment *)
    55.5 -nonfix ++ -- RL mem;
    55.6 +nonfix ++ -- RL;
    55.7  val explode = String.explode;
    55.8  val implode = String.implode;
    55.9  val print = TextIO.print;
    56.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Thu May 06 08:43:51 2010 +0200
    56.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Thu May 06 08:44:19 2010 +0200
    56.3 @@ -82,7 +82,7 @@
    56.4    -- Scan.many (not o Symbol.is_ascii_blank o symbol)
    56.5    >> (token AsciiSymbol o op ::);
    56.6  
    56.7 -fun not_contains xs c = not ((symbol c) mem_string (explode xs));
    56.8 +fun not_contains xs c = not (member (op =) (explode xs) (symbol c));
    56.9  val scan_comment =
   56.10    $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   56.11    >> token Comment;
    57.1 --- a/src/ZF/Tools/datatype_package.ML	Thu May 06 08:43:51 2010 +0200
    57.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu May 06 08:44:19 2010 +0200
    57.3 @@ -58,7 +58,7 @@
    57.4              @{const_name nat} :: map (#1 o dest_Const) rec_hds
    57.5          val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
    57.6          val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
    57.7 -          (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
    57.8 +          (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
    57.9              | _ => I)) con_ty_lists [];
   57.10      in  u $ Ind_Syntax.union_params (hd rec_tms, cs)  end;
   57.11  
   57.12 @@ -193,7 +193,7 @@
   57.13      | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) =
   57.14         (case head_of X of
   57.15              Const(a,_) => (*recursive occurrence?*)
   57.16 -                          if a mem_string rec_names
   57.17 +                          if member (op =) rec_names a
   57.18                                then arg :: rec_args prems
   57.19                            else rec_args prems
   57.20            | _ => rec_args prems)
    58.1 --- a/src/ZF/Tools/inductive_package.ML	Thu May 06 08:43:51 2010 +0200
    58.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu May 06 08:44:19 2010 +0200
    58.3 @@ -86,7 +86,7 @@
    58.4    local (*Checking the introduction rules*)
    58.5      val intr_sets = map (#2 o rule_concl_msg thy) intr_tms;
    58.6      fun intr_ok set =
    58.7 -        case head_of set of Const(a,recT) => a mem rec_names | _ => false;
    58.8 +        case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
    58.9    in
   58.10      val dummy =  assert_all intr_ok intr_sets
   58.11         (fn t => "Conclusion of rule does not name a recursive set: " ^