# HG changeset patch # User haftmann # Date 1273128259 -7200 # Node ID 40dcc319d4cd5a22342db706aa2a0782d1bc075c # Parent 842fdcd421598bb7ec09891451de74048ec4500c# Parent 54b64d4ad52417327e0dc19829893a52c4bf1794 merged diff -r 842fdcd42159 -r 40dcc319d4cd src/FOLP/hypsubst.ML --- a/src/FOLP/hypsubst.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/FOLP/hypsubst.ML Thu May 06 08:44:19 2010 +0200 @@ -33,7 +33,7 @@ exception EQ_VAR; -fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); +fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0; (*It's not safe to substitute for a constant; consider 0=1. It's not safe to substitute for x=t[x] since x is not eliminated. diff -r 842fdcd42159 -r 40dcc319d4cd src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/FOLP/simp.ML Thu May 06 08:44:19 2010 +0200 @@ -98,7 +98,7 @@ in var(lhs_of_eq i thm) end; fun contains_op opns = - let fun contains(Const(s,_)) = s mem opns | + let fun contains(Const(s,_)) = member (op =) opns s | contains(s$t) = contains s orelse contains t | contains(Abs(_,_,t)) = contains t | contains _ = false; @@ -117,7 +117,7 @@ in map norm normE_thms end; fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of - Const(s,_)$_ => s mem norms | _ => false; + Const(s,_)$_ => member (op =) norms s | _ => false; val refl_tac = resolve_tac refl_thms; @@ -203,7 +203,7 @@ val refl1_tac = refl_tac 1 fun norm_step_tac st = st |> (case head_of(rhs_of_eq 1 st) of - Var(ixn,_) => if ixn mem hvs then refl1_tac + Var(ixn,_) => if member (op =) hvs ixn then refl1_tac else resolve_tac normI_thms 1 ORELSE refl1_tac | Const _ => resolve_tac normI_thms 1 ORELSE resolve_tac congs 1 ORELSE refl1_tac diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu May 06 08:44:19 2010 +0200 @@ -46,7 +46,7 @@ val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) fun mk_all ((s, T), (P,n)) = - if 0 mem loose_bnos P then + if member (op =) (loose_bnos P) 0 then (HOLogic.all_const T $ Abs (s, T, P), n) else (incr_boundvars ~1 P, n-1) fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Thu May 06 08:44:19 2010 +0200 @@ -51,7 +51,7 @@ val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) fun mk_all ((s, T), (P,n)) = - if 0 mem loose_bnos P then + if member (op =) (loose_bnos P) 0 then (HOLogic.all_const T $ Abs (s, T, P), n) else (incr_boundvars ~1 P, n-1) fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Thu May 06 08:44:19 2010 +0200 @@ -66,7 +66,7 @@ val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) fun mk_all ((s, T), (P,n)) = - if 0 mem loose_bnos P then + if member (op =) (loose_bnos P) 0 then (HOLogic.all_const T $ Abs (s, T, P), n) else (incr_boundvars ~1 P, n-1) fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/HOL.thy Thu May 06 08:44:19 2010 +0200 @@ -1963,7 +1963,7 @@ text {* Avoid some named infixes in evaluation environment *} -code_reserved Eval oo ooo oooo upto downto orf andf mem mem_int mem_string +code_reserved Eval oo ooo oooo upto downto orf andf setup {* Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Import/hol4rews.ML Thu May 06 08:44:19 2010 +0200 @@ -604,9 +604,9 @@ val defname = Thm.def_name name val pdefname = name ^ "_primdef" in - if not (defname mem used) + if not (member (op =) used defname) then F defname (* name_def *) - else if not (pdefname mem used) + else if not (member (op =) used pdefname) then F pdefname (* name_primdef *) else F (Name.variant used pdefname) (* last resort *) end diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Thu May 06 08:44:19 2010 +0200 @@ -276,6 +276,7 @@ in F end +infix mem; fun i mem L = let fun itr [] = false | itr (a::rst) = i=a orelse itr rst @@ -1091,7 +1092,7 @@ let fun F vars (Bound _) = vars | F vars (tm as Free _) = - if tm mem vars + if member (op =) vars tm then vars else (tm::vars) | F vars (Const _) = vars diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Import/shuffler.ML Thu May 06 08:44:19 2010 +0200 @@ -550,7 +550,7 @@ fun match_consts ignore t (* th *) = let fun add_consts (Const (c, _), cs) = - if c mem_string ignore + if member (op =) ignore c then cs else insert (op =) c cs | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 08:44:19 2010 +0200 @@ -528,8 +528,8 @@ end end; -fun isspace x = x = " " ; -fun isnum x = x mem_string ["0","1","2","3","4","5","6","7","8","9"] +fun isspace x = (x = " "); +fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x; (* More parser basics. *) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Library/normarith.ML Thu May 06 08:44:19 2010 +0200 @@ -311,7 +311,7 @@ in forall (fn e => evaluate f e =/ Rat.zero) flippedequations end val goodverts = filter check_solution rawverts - val signfixups = map (fn n => if n mem_int f then ~1 else 1) nvs + val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts end val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Library/reflection.ML Thu May 06 08:44:19 2010 +0200 @@ -149,7 +149,7 @@ Pattern.match thy ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) (Vartab.empty, Vartab.empty) - val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) + val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv) val (fts,its) = (map (snd o snd) fnvs, map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu May 06 08:44:19 2010 +0200 @@ -921,7 +921,7 @@ check_finity gl bl ((t,cl)::r) b = let fun listmem [] _ = true | -listmem (a::r) l = if (a mem l) then (listmem r l) else false; +listmem (a::r) l = if member (op =) l a then (listmem r l) else false; fun snd_listmem [] _ = true | snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false; in @@ -966,7 +966,7 @@ (ll @ (new_types r)) end; in - if (a mem done) + if member (op =) done a then (preprocess_td sg b done) else (let diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Thu May 06 08:44:19 2010 +0200 @@ -361,7 +361,7 @@ val t' = canonize_term t comms; val u' = canonize_term u comms; in - if s mem comms andalso Term_Ord.termless (u', t') + if member (op =) comms s andalso Term_Ord.termless (u', t') then Const (s, T) $ u' $ t' else Const (s, T) $ t' $ u' end diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu May 06 08:44:19 2010 +0200 @@ -218,8 +218,8 @@ fun is_forbidden_theorem (s, th) = let val consts = Term.add_const_names (prop_of th) [] in - exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse - exists (fn s' => s' mem forbidden_consts) consts orelse + exists (member (op =) (space_explode "." s)) forbidden_thms orelse + exists (member (op =) forbidden_consts) consts orelse length (space_explode "." s) <> 2 orelse String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse String.isSuffix "_def" s orelse diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu May 06 08:44:19 2010 +0200 @@ -66,7 +66,7 @@ fun mk_case_names_exhausts descr new = map (Rule_Cases.case_names o exhaust_cases descr o #1) - (filter (fn ((_, (name, _, _))) => name mem_string new) descr); + (filter (fn ((_, (name, _, _))) => member (op =) new name) descr); end; @@ -131,7 +131,7 @@ let val (aT as Type (a, []), S) = dest_permT T; val (bT as Type (b, []), _) = dest_permT U - in if aT mem permTs_of u andalso aT <> bT then + in if member (op =) (permTs_of u) aT andalso aT <> bT then let val cp = cp_inst_of thy a b; val dj = dj_thm_of thy b a; @@ -1772,7 +1772,7 @@ val params' = params1 @ params2; val rec_prems = filter (fn th => case prop_of th of _ $ p => (case head_of p of - Const (s, _) => s mem rec_set_names + Const (s, _) => member (op =) rec_set_names s | _ => false) | _ => false) prems'; val fresh_prems = filter (fn th => case prop_of th of diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu May 06 08:44:19 2010 +0200 @@ -43,7 +43,7 @@ fun mk_perm_bool_simproc names = Simplifier.simproc_i (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => fn Const ("Nominal.perm", _) $ _ $ t => - if the_default "" (try (head_of #> dest_Const #> fst) t) mem names + if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE | _ => NONE); @@ -73,7 +73,7 @@ fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (f p q) else NONE + if member (op =) names name then SOME (f p q) else NONE | _ => NONE) | split_conj _ _ _ _ = NONE; @@ -92,7 +92,7 @@ fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (HOLogic.mk_conj (p, + if member (op =) names name then SOME (HOLogic.mk_conj (p, Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ (subst_bounds (pis, strip_all pis q)))) else NONE @@ -214,7 +214,7 @@ fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in - if p mem ps then + if member (op =) ps p then Const (inductive_forall_name, (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) @@ -510,7 +510,7 @@ val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis); val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms (fn x as Free _ => - if x mem args then x + if member (op =) args x then x else (case AList.lookup op = tab x of SOME y => y | NONE => fold_rev (NominalDatatype.mk_perm []) pis x) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Thu May 06 08:44:19 2010 +0200 @@ -46,7 +46,7 @@ fun mk_perm_bool_simproc names = Simplifier.simproc_i (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => fn Const ("Nominal.perm", _) $ _ $ t => - if the_default "" (try (head_of #> dest_Const #> fst) t) mem names + if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE | _ => NONE); @@ -77,7 +77,7 @@ fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (f p q) else NONE + if member (op =) names name then SOME (f p q) else NONE | _ => NONE) | split_conj _ _ _ _ = NONE; @@ -96,7 +96,7 @@ fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (HOLogic.mk_conj (p, + if member (op =) names name then SOME (HOLogic.mk_conj (p, Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ (subst_bounds (pis, strip_all pis q)))) else NONE @@ -239,7 +239,7 @@ fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in - if p mem ps then + if member (op =) ps p then Const (inductive_forall_name, (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Statespace/state_space.ML Thu May 06 08:44:19 2010 +0200 @@ -528,7 +528,7 @@ | dups => ["Duplicate renaming(s) for " ^ commas dups]) val cnames = map fst components; - val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of + val err_rename_unknowns = (case subtract (op =) cnames rnames of [] => [] | rs => ["Unknown components " ^ commas rs]); diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu May 06 08:44:19 2010 +0200 @@ -309,7 +309,7 @@ val T' = typ_of_dtyp descr' sorts dt; val (Us, U) = strip_type T' in (case strip_dtyp dt of - (_, DtRec j) => if j mem ks' then + (_, DtRec j) => if member (op =) ks' j then (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us], Ts @ [Us ---> Univ_elT]) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu May 06 08:44:19 2010 +0200 @@ -136,7 +136,7 @@ val getP = if can HOLogic.dest_imp (hd ts) then (apfst SOME) o HOLogic.dest_imp else pair NONE; val flt = if null indnames then I else - filter (fn Free (s, _) => s mem indnames | _ => false); + filter (fn Free (s, _) => member (op =) indnames s | _ => false); fun abstr (t1, t2) = (case t1 of NONE => (case flt (OldTerm.term_frees t2) of [Free (s, T)] => SOME (absfree (s, T, t2)) @@ -300,7 +300,7 @@ fun is_nonempty_dt is i = let val (_, _, constrs) = (the o AList.lookup (op =) descr') i; - fun arg_nonempty (_, DtRec i) = if i mem is then false + fun arg_nonempty (_, DtRec i) = if member (op =) is i then false else is_nonempty_dt (i::is) i | arg_nonempty _ = true; in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 06 08:44:19 2010 +0200 @@ -306,11 +306,11 @@ map_node node_id (K (NONE, module', string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ [str ";"])) ^ "\n\n" ^ - (if "term_of" mem !mode then + (if member (op =) (!mode) "term_of" then string_of (Pretty.blk (0, separate Pretty.fbrk (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" else "") ^ - (if "test" mem !mode then + (if member (op =) (!mode) "test" then string_of (Pretty.blk (0, separate Pretty.fbrk (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" else ""))) gr2 diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu May 06 08:44:19 2010 +0200 @@ -41,16 +41,16 @@ else map (fn i => "P" ^ string_of_int i) (1 upto length descr); val rec_result_Ts = map (fn ((i, _), P) => - if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT) + if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT) (descr ~~ pnames); fun make_pred i T U r x = - if i mem is then + if member (op =) is i then Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x; fun mk_all i s T t = - if i mem is then list_all_free ([(s, T)], t) else t; + if member (op =) is i then list_all_free ([(s, T)], t) else t; val (prems, rec_fns) = split_list (flat (fst (fold_map (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j => @@ -66,7 +66,7 @@ val vs' = filter_out is_unit vs; val f = mk_Free "f" (map fastype_of vs' ---> rT) j; val f' = Envir.eta_contract (list_abs_free - (map dest_Free vs, if i mem is then list_comb (f, vs') + (map dest_Free vs, if member (op =) is i then list_comb (f, vs') else HOLogic.unit)); in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs')) (list_comb (Const (cname, Ts ---> T), map Free frees))), f') @@ -100,7 +100,7 @@ (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); val r = if null is then Extraction.nullt else foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) => - if i mem is then SOME + if member (op =) is i then SOME (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"}) @@ -131,7 +131,7 @@ val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []); val rvs = rev (Thm.fold_terms Term.add_vars thm' []); val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *) - tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs); + member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs; val prf = diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Thu May 06 08:44:19 2010 +0200 @@ -244,7 +244,7 @@ val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq - val _ = fname mem fnames + val _ = member (op =) fnames fname orelse input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames) @@ -259,7 +259,7 @@ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") val _ = forall (not o Term.exists_subterm - (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args) + (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) orelse input_error "Defined function may not occur in premises or arguments" val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 06 08:44:19 2010 +0200 @@ -2178,7 +2178,7 @@ val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) val (c, _) = strip_comb t in (case c of - Const (name, _) => name mem_string constr_consts + Const (name, _) => member (op =) constr_consts name | _ => false) end)) else false diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu May 06 08:44:19 2010 +0200 @@ -538,6 +538,8 @@ open Generated_Cooper; +fun member eq = Library.member eq; + fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s); fun i_of_term vs t = case t of Free (xn, xT) => (case AList.lookup (op aconv) vs t @@ -593,12 +595,12 @@ in fun term_bools acc t = case t of - (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b + (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b else insert (op aconv) t acc - | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a + | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a else insert (op aconv) t acc | Abs p => term_bools acc (snd (variant_abs p)) - | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc + | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc end; fun myassoc2 l v = diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Qelim/presburger.ML Thu May 06 08:44:19 2010 +0200 @@ -67,9 +67,9 @@ | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t fun ty cts t = - if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false + if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false else case term_of t of - c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] + c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c then not (isnum l orelse isnum r) else not (member (op aconv) cts c) | c$_ => not (member (op aconv) cts c) @@ -85,8 +85,8 @@ in fun is_relevant ctxt ct = subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt)) - andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct)) - andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct)); + andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct)) + andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct)); fun int_nat_terms ctxt ct = let diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu May 06 08:44:19 2010 +0200 @@ -728,7 +728,7 @@ val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos val ty_substs = if qtys = [] then all_ty_substs else - filter (fn (_, qty) => qty mem qtys) all_ty_substs + filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu May 06 08:44:19 2010 +0200 @@ -387,7 +387,7 @@ (*Ignore blacklisted basenames*) fun add_multi_names (a, ths) pairs = - if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs + if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs else add_single_names (a, ths) pairs; fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu May 06 08:44:19 2010 +0200 @@ -410,7 +410,7 @@ | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) arity_clause dfg seen n (tcons,ars) | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) = - if class mem_string seen then (*multiple arities for the same tycon, class pair*) + if member (op =) seen class then (*multiple arities for the same tycon, class pair*) make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: arity_clause dfg seen (n+1) (tcons,ars) else diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Thu May 06 08:44:19 2010 +0200 @@ -76,7 +76,7 @@ let val slist = Unsynchronized.ref names val vname = Unsynchronized.ref "u" fun new() = - if !vname mem_string (!slist) + if member (op =) (!slist) (!vname) then (vname := Symbol.bump_string (!vname); new()) else (slist := !vname :: !slist; !vname) in diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Thu May 06 08:44:19 2010 +0200 @@ -122,7 +122,7 @@ | dual x = HOLogic.Not $ x (* Term.term list -> bool *) fun has_duals [] = false - | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs + | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs in has_duals (HOLogic.disjuncts c) end; diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/hologic.ML Thu May 06 08:44:19 2010 +0200 @@ -356,7 +356,7 @@ fun mk_ptupleT ps = let fun mk p Ts = - if p mem ps then + if member (op =) ps p then let val (T, Ts') = mk (1::p) Ts; val (U, Ts'') = mk (2::p) Ts' @@ -366,7 +366,7 @@ fun strip_ptupleT ps = let - fun factors p T = if p mem ps then (case T of + fun factors p T = if member (op =) ps p then (case T of Type ("*", [T1, T2]) => factors (1::p) T1 @ factors (2::p) T2 | _ => ptuple_err "strip_ptupleT") else [T] @@ -382,7 +382,7 @@ fun mk_ptuple ps = let fun mk p T ts = - if p mem ps then (case T of + if member (op =) ps p then (case T of Type ("*", [T1, T2]) => let val (t, ts') = mk (1::p) T1 ts; @@ -394,7 +394,7 @@ fun strip_ptuple ps = let - fun dest p t = if p mem ps then (case t of + fun dest p t = if member (op =) ps p then (case t of Const ("Pair", _) $ t $ u => dest (1::p) t @ dest (2::p) u | _ => ptuple_err "strip_ptuple") else [t] @@ -413,7 +413,7 @@ fun mk_psplits ps T T3 u = let fun ap ((p, T) :: pTs) = - if p mem ps then (case T of + if member (op =) ps p then (case T of Type ("*", [T1, T2]) => split_const (T1, T2, map snd pTs ---> T3) $ ap ((1::p, T1) :: (2::p, T2) :: pTs) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Thu May 06 08:44:19 2010 +0200 @@ -288,7 +288,7 @@ then err bad_ind_occ else (); fun check_prem' prem t = - if head_of t mem cs then + if member (op =) cs (head_of t) then check_ind (err_in_prem ctxt err_name rule prem) t else (case t of Abs (_, _, t) => check_prem' prem t @@ -301,7 +301,7 @@ in (case concl of Const (@{const_name Trueprop}, _) $ t => - if head_of t mem cs then + if member (op =) cs (head_of t) then (check_ind (err_in_rule ctxt err_name rule') t; List.app check_prem (prems ~~ aprems)) else err_in_rule ctxt err_name rule' bad_concl diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Thu May 06 08:44:19 2010 +0200 @@ -140,7 +140,7 @@ fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm []; fun get_args _ _ [] = ([], []) - | get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x) + | get_args is i (x::xs) = (if member (op =) is i then apfst else apsnd) (cons x) (get_args is (i+1) xs); fun merge xs [] = xs @@ -237,7 +237,7 @@ end) ps)); -fun use_random () = "random_ind" mem !Codegen.mode; +fun use_random () = member (op =) (!Codegen.mode) "random_ind"; fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) = let @@ -557,7 +557,7 @@ fun mk_extra_defs thy defs gr dep names module ts = fold (fn name => fn gr => - if name mem names then gr + if member (op =) names name then gr else (case get_clauses thy name of NONE => gr @@ -576,7 +576,7 @@ val args = List.take (snd (strip_comb u), nparms); val arg_vs = maps term_vs args; - fun get_nparms s = if s mem names then SOME nparms else + fun get_nparms s = if member (op =) names s then SOME nparms else Option.map #3 (get_clauses thy s); fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) = @@ -585,7 +585,7 @@ Prem ([t, u], eq, false) | dest_prem (_ $ t) = (case strip_comb t of - (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t + (v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t | (c as Const (s, _), ts) => (case get_nparms s of NONE => Sidecond t @@ -704,7 +704,7 @@ val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); val xs' = map (fn Bound i => nth xs (k - i)) ts; fun conv xs js = - if js mem fs then + if member (op =) fs js then let val (p, xs') = conv xs (1::js); val (q, xs'') = conv xs' (2::js) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Thu May 06 08:44:19 2010 +0200 @@ -57,7 +57,7 @@ fun relevant_vars prop = List.foldr (fn (Var ((a, i), T), vs) => (case strip_type T of - (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs + (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs | _ => vs) | (_, vs) => vs) [] (OldTerm.term_vars prop); @@ -90,7 +90,7 @@ val xs = map (pair "x") Ts; val u = list_comb (t, map Bound (i - 1 downto 0)) in - if a mem vs then + if member (op =) vs a then list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u) else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u) end @@ -257,7 +257,7 @@ let val rvs = map fst (relevant_vars (prop_of rule)); val xs = rev (Term.add_vars (prop_of rule) []); - val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs); + val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs); val rlzvs = rev (Term.add_vars (prop_of rrule) []); val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; val rs = map Var (subtract (op = o pairself fst) xs rlzvs); @@ -292,7 +292,7 @@ Sign.root_path |> Sign.add_path (Long_Name.implode prfx); val (ty_eqs, rlz_eqs) = split_list - (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss); + (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss); val thy1' = thy1 |> Theory.copy |> @@ -300,7 +300,7 @@ fold (fn s => AxClass.axiomatize_arity (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> Extraction.add_typeof_eqns_i ty_eqs; - val dts = map_filter (fn (s, rs) => if s mem rsets then + val dts = map_filter (fn (s, rs) => if member (op =) rsets s then SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; (** datatype representing computational content of inductive set **) @@ -363,7 +363,7 @@ (** realizer for induction rule **) - val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then + val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then SOME (fst (fst (dest_Var (head_of P)))) else NONE) (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); @@ -471,7 +471,7 @@ list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) [])))))) (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4; val elimps = map_filter (fn ((s, intrs), p) => - if s mem rsets then SOME (p, intrs) else NONE) + if member (op =) rsets s then SOME (p, intrs) else NONE) (rss' ~~ (elims ~~ #elims ind_info)); val thy6 = fold (fn p as (((((elim, _), _), _), _), _) => diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Thu May 06 08:44:19 2010 +0200 @@ -419,7 +419,7 @@ | infer (t $ u) = infer t #> infer u | infer _ = I; val new_arities = filter_out - (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1 + (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 1 | _ => false) (fold (snd #> infer) intros []); val params' = map (fn x => (case AList.lookup op = new_arities x of diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/lin_arith.ML Thu May 06 08:44:19 2010 +0200 @@ -221,7 +221,7 @@ in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end handle TERM _ => add_atom all m pi) | poly (all as Const f $ x, m, pi) = - if f mem inj_consts then poly (x, m, pi) else add_atom all m pi + if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi | poly (all, m, pi) = add_atom all m pi val (p, i) = poly (lhs, Rat.one, ([], Rat.zero)) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/old_primrec.ML Thu May 06 08:44:19 2010 +0200 @@ -120,7 +120,7 @@ let val (f, ts) = strip_comb t; in - if is_Const f andalso dest_Const f mem map fst rec_eqns then + if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then let val fnameT' as (fname', _) = dest_Const f; val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT'); diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Thu May 06 08:44:19 2010 +0200 @@ -114,7 +114,7 @@ in (case xs of [_] => (module, put_code module fundef gr2) | _ => - if not (dep mem xs) then + if not (member (op =) xs dep) then let val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; val module' = if_library thyname module; diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/refute.ML Thu May 06 08:44:19 2010 +0200 @@ -463,7 +463,7 @@ in (* I'm not quite sure if checking the name 's' is sufficient, *) (* or if we should also check the type 'T'. *) - s mem_string class_const_names + member (op =) class_const_names s end; (* ------------------------------------------------------------------------- *) @@ -499,7 +499,7 @@ in (* I'm not quite sure if checking the name 's' is sufficient, *) (* or if we should also check the type 'T'. *) - s mem_string rec_names + member (op =) rec_names s end; (* ------------------------------------------------------------------------- *) @@ -932,7 +932,7 @@ | Datatype_Aux.DtType (_, ds) => collect_types dT (fold_rev collect_dtyp ds acc) | Datatype_Aux.DtRec i => - if dT mem acc then + if member (op =) acc dT then acc (* prevent infinite recursion *) else let @@ -2248,7 +2248,7 @@ (* if 't_elem' existed at the previous depth, *) (* proceed recursively, otherwise map the entire *) (* subtree to "undefined" *) - if t_elem mem terms' then + if member (op =) terms' t_elem then make_constr ds off else (make_undef ds, off)) diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/sat_solver.ML Thu May 06 08:44:19 2010 +0200 @@ -350,7 +350,7 @@ o (map (map literal_from_int)) o clauses o (map int_from_string) - o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"]))) + o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"]))) o filter_preamble o filter (fn l => l <> "") o split_lines @@ -421,7 +421,7 @@ SOME (y::x::xs) (* int list -> int -> bool *) fun assignment_from_list xs i = - i mem xs + member (op =) xs i (* int list -> SatSolver.result *) fun solver_loop xs = if PropLogic.eval (assignment_from_list xs) fm then @@ -490,7 +490,7 @@ end (* int list -> int option *) fun fresh_var xs = - Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices + find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices (* int list -> prop_formula -> int list option *) (* partial assignment 'xs' *) fun dpll xs fm = diff -r 842fdcd42159 -r 40dcc319d4cd src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Thu May 06 08:44:19 2010 +0200 @@ -78,7 +78,7 @@ Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, Codegen.str "x) = x;"]) ^ "\n\n" ^ - (if "term_of" mem !Codegen.mode then + (if member (op =) (!Codegen.mode) "term_of" then Codegen.string_of (Pretty.block [Codegen.str "fun ", Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, @@ -89,7 +89,7 @@ Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, Codegen.str "x;"]) ^ "\n\n" else "") ^ - (if "test" mem !Codegen.mode then + (if member (op =) (!Codegen.mode) "test" then Codegen.string_of (Pretty.block [Codegen.str "fun ", Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, Codegen.str "i =", Pretty.brk 1, diff -r 842fdcd42159 -r 40dcc319d4cd src/HOLCF/IOA/ABP/Check.ML --- a/src/HOLCF/IOA/ABP/Check.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOLCF/IOA/ABP/Check.ML Thu May 06 08:44:19 2010 +0200 @@ -16,7 +16,7 @@ let fun check_s(s,unchecked,checked) = let fun check_sa a unchecked = let fun check_sas t unchecked = - (if a mem extacts then + (if member (op =) extacts a then (if transA(hom s,a,hom t) then ( ) else (writeln("Error: Mapping of Externals!"); string_of_s s; writeln""; @@ -27,11 +27,11 @@ string_of_s s; writeln""; string_of_a a; writeln""; string_of_s t;writeln"";writeln"" )); - if t mem checked then unchecked else insert (op =) t unchecked) + if member (op =) checked t then unchecked else insert (op =) t unchecked) in fold check_sas (nexts s a) unchecked end; val unchecked' = fold check_sa (extacts @ intacts) unchecked - in (if s mem startsI then - (if hom(s) mem startsS then () + in (if member (op =) startsI s then + (if member (op =) startsS (hom s) then () else writeln("Error: At start states!")) else (); checks(unchecked',s::checked)) end diff -r 842fdcd42159 -r 40dcc319d4cd src/HOLCF/IOA/meta_theory/automaton.ML --- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML Thu May 06 08:44:19 2010 +0200 @@ -211,11 +211,11 @@ (* used by write_alts *) fun write_alt thy (chead,tr) inp out int [] = -if (chead mem inp) then +if member (op =) inp chead then ( error("Input action " ^ tr ^ " was not specified") ) else ( -if (chead mem (out@int)) then +if member (op =) out chead orelse member (op =) int chead then (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); (tr ^ " => False",tr ^ " => False")) | write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = @@ -227,9 +227,9 @@ occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); in if (chead=(hd_of a)) then -(if ((chead mem inp) andalso e) then ( +(if member (op =) inp chead andalso e then ( error("Input action " ^ b ^ " has a precondition") -) else (if (chead mem (inp@out@int)) then +) else (if member (op =) (inp@out@int) chead then (if (occurs_again chead r) then ( error("Two specifications for action: " ^ b) ) else (b ^ " => " ^ c,b ^ " => " ^ d)) @@ -275,7 +275,7 @@ check_free_primed _ = []; fun overlap [] _ = true | -overlap (a::r) l = if (a mem l) then ( +overlap (a::r) l = if member (op =) l a then ( error("Two occurences of action " ^ a ^ " in automaton signature") ) else (overlap r l); diff -r 842fdcd42159 -r 40dcc319d4cd src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu May 06 08:44:19 2010 +0200 @@ -228,7 +228,7 @@ fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = (case cont_eta_contract body of body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (0 mem loose_bnos f) then incr_boundvars ~1 f + if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t diff -r 842fdcd42159 -r 40dcc319d4cd src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu May 06 08:44:19 2010 +0200 @@ -554,9 +554,9 @@ (* test for finiteness of domain definitions *) local val types = [@{type_name ssum}, @{type_name sprod}]; - fun finite d T = if T mem absTs then d else finite' d T + fun finite d T = if member (op =) absTs T then d else finite' d T and finite' d (Type (c, Ts)) = - let val d' = d andalso c mem types; + let val d' = d andalso member (op =) types c; in forall (finite d') Ts end | finite' d _ = true; in diff -r 842fdcd42159 -r 40dcc319d4cd src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 06 08:44:19 2010 +0200 @@ -292,7 +292,7 @@ it has a possibly indirectly recursive argument that isn't/is possibly indirectly lazy *) fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => - is_rec arg andalso not(rec_of arg mem ns) andalso + is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) diff -r 842fdcd42159 -r 40dcc319d4cd src/Provers/Arith/cancel_div_mod.ML --- a/src/Provers/Arith/cancel_div_mod.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Provers/Arith/cancel_div_mod.ML Thu May 06 08:44:19 2010 +0200 @@ -62,7 +62,7 @@ let val ts = Data.dest_sum t; val dpq = Data.mk_binop Data.div_name pq val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq) - val d = if d1 mem ts then d1 else d2 + val d = if member (op =) ts d1 then d1 else d2 val m = Data.mk_binop Data.mod_name pq in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end diff -r 842fdcd42159 -r 40dcc319d4cd src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Thu May 06 08:44:19 2010 +0200 @@ -389,7 +389,7 @@ |> sort (int_ord o pairself abs) |> hd val (eq as Lineq(_,_,ceq,_),othereqs) = - extract_first (fn Lineq(_,_,l,_) => c mem l) eqs + extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs val v = find_index (fn v => v = c) ceq val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) (othereqs @ noneqs) diff -r 842fdcd42159 -r 40dcc319d4cd src/Provers/order.ML --- a/src/Provers/order.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Provers/order.ML Thu May 06 08:44:19 2010 +0200 @@ -871,8 +871,8 @@ val vi = getIndex v ntc in - if ui mem xreachable andalso vi mem xreachable andalso - ui mem yreachable andalso vi mem yreachable then ( + if member (op =) xreachable ui andalso member (op =) xreachable vi andalso + member (op =) yreachable ui andalso member (op =) yreachable vi then ( (case e of (Less (_, _, _)) => let diff -r 842fdcd42159 -r 40dcc319d4cd src/Provers/trancl.ML --- a/src/Provers/trancl.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Provers/trancl.ML Thu May 06 08:44:19 2010 +0200 @@ -452,8 +452,8 @@ fun processTranclEdges [] = raise Cannot | processTranclEdges (e::es) = - if (upper e) mem Vx andalso (lower e) mem Vx - andalso (upper e) mem Vy andalso (lower e) mem Vy + if member (op =) Vx (upper e) andalso member (op =) Vx (lower e) + andalso member (op =) Vy (upper e) andalso member (op =) Vy (lower e) then ( diff -r 842fdcd42159 -r 40dcc319d4cd src/Pure/ProofGeneral/pgip_input.ML --- a/src/Pure/ProofGeneral/pgip_input.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Pure/ProofGeneral/pgip_input.ML Thu May 06 08:44:19 2010 +0200 @@ -227,8 +227,8 @@ (* We allow sending proper document markup too; we map it back to dostep *) (* and strip out metainfo elements. Markup correctness isn't checked: this *) (* is a compatibility measure to make it easy for interfaces. *) - | x => if (x mem PgipMarkup.doc_markup_elements) then - if (x mem PgipMarkup.doc_markup_elements_ignored) then + | x => if member (op =) PgipMarkup.doc_markup_elements x then + if member (op =) PgipMarkup.doc_markup_elements_ignored x then raise NoAction else Dostep { text = xmltext data } (* could separate out Doitem too *) diff -r 842fdcd42159 -r 40dcc319d4cd src/Pure/library.ML --- a/src/Pure/library.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Pure/library.ML Thu May 06 08:44:19 2010 +0200 @@ -11,7 +11,7 @@ infix 2 ? infix 3 o oo ooo oooo infix 4 ~~ upto downto -infix orf andf mem mem_int mem_string +infix orf andf signature BASIC_LIBRARY = sig @@ -164,9 +164,6 @@ val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list - val mem: ''a * ''a list -> bool - val mem_int: int * int list -> bool - val mem_string: string * string list -> bool val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool val distinct: ('a * 'a -> bool) -> 'a list -> 'a list @@ -801,13 +798,6 @@ else fold_rev (insert eq) ys xs; -(* old-style infixes *) - -fun x mem xs = member (op =) xs x; -fun (x: int) mem_int xs = member (op =) xs x; -fun (x: string) mem_string xs = member (op =) xs x; - - (* subset and set equality *) fun subset eq (xs, ys) = forall (member eq ys) xs; diff -r 842fdcd42159 -r 40dcc319d4cd src/Tools/Metis/metis_env.ML --- a/src/Tools/Metis/metis_env.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Tools/Metis/metis_env.ML Thu May 06 08:44:19 2010 +0200 @@ -1,5 +1,5 @@ (* Metis-specific ML environment *) -nonfix ++ -- RL mem; +nonfix ++ -- RL; val explode = String.explode; val implode = String.implode; val print = TextIO.print; diff -r 842fdcd42159 -r 40dcc319d4cd src/Tools/WWW_Find/unicode_symbols.ML --- a/src/Tools/WWW_Find/unicode_symbols.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/Tools/WWW_Find/unicode_symbols.ML Thu May 06 08:44:19 2010 +0200 @@ -82,7 +82,7 @@ -- Scan.many (not o Symbol.is_ascii_blank o symbol) >> (token AsciiSymbol o op ::); -fun not_contains xs c = not ((symbol c) mem_string (explode xs)); +fun not_contains xs c = not (member (op =) (explode xs) (symbol c)); val scan_comment = $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n")) >> token Comment; diff -r 842fdcd42159 -r 40dcc319d4cd src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/ZF/Tools/datatype_package.ML Thu May 06 08:44:19 2010 +0200 @@ -58,7 +58,7 @@ @{const_name nat} :: map (#1 o dest_Const) rec_hds val u = if co then @{const QUniv.quniv} else @{const Univ.univ} val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) - (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t + (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t | _ => I)) con_ty_lists []; in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; @@ -193,7 +193,7 @@ | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) = (case head_of X of Const(a,_) => (*recursive occurrence?*) - if a mem_string rec_names + if member (op =) rec_names a then arg :: rec_args prems else rec_args prems | _ => rec_args prems) diff -r 842fdcd42159 -r 40dcc319d4cd src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu May 06 08:43:51 2010 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu May 06 08:44:19 2010 +0200 @@ -86,7 +86,7 @@ local (*Checking the introduction rules*) val intr_sets = map (#2 o rule_concl_msg thy) intr_tms; fun intr_ok set = - case head_of set of Const(a,recT) => a mem rec_names | _ => false; + case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false; in val dummy = assert_all intr_ok intr_sets (fn t => "Conclusion of rule does not name a recursive set: " ^