farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
--- a/src/FOLP/hypsubst.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/FOLP/hypsubst.ML Wed May 05 18:25:34 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.
--- a/src/FOLP/simp.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/FOLP/simp.ML Wed May 05 18:25:34 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
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed May 05 18:25:34 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;
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed May 05 18:25:34 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;
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed May 05 18:25:34 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;
--- a/src/HOL/HOL.thy Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/HOL.thy Wed May 05 18:25:34 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)
--- a/src/HOL/Import/hol4rews.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Wed May 05 18:25:34 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
--- a/src/HOL/Import/proof_kernel.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed May 05 18:25:34 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
--- a/src/HOL/Import/shuffler.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Wed May 05 18:25:34 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))
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed May 05 18:25:34 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. *)
--- a/src/HOL/Library/normarith.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Library/normarith.ML Wed May 05 18:25:34 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)) []
--- a/src/HOL/Library/reflection.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Library/reflection.ML Wed May 05 18:25:34 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)
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed May 05 18:25:34 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
--- a/src/HOL/Mutabelle/mutabelle.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Wed May 05 18:25:34 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
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed May 05 18:25:34 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
--- a/src/HOL/Nominal/nominal_datatype.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed May 05 18:25:34 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
--- a/src/HOL/Nominal/nominal_inductive.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed May 05 18:25:34 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)
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed May 05 18:25:34 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))
--- a/src/HOL/Statespace/state_space.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed May 05 18:25:34 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]);
--- a/src/HOL/Tools/Datatype/datatype.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed May 05 18:25:34 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])
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed May 05 18:25:34 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 =
--- a/src/HOL/Tools/Function/function_common.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/Qelim/cooper.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed May 05 18:25:34 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 =
--- a/src/HOL/Tools/Qelim/presburger.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/Quotient/quotient_term.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed May 05 18:25:34 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;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/TFL/tfl.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/cnf_funcs.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Wed May 05 18:25:34 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;
--- a/src/HOL/Tools/hologic.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Wed May 05 18:25:34 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)
--- a/src/HOL/Tools/inductive.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/inductive_codegen.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed May 05 18:25:34 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)
--- a/src/HOL/Tools/inductive_realizer.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed May 05 18:25:34 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, _), _), _), _), _) =>
--- a/src/HOL/Tools/inductive_set.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed May 05 18:25:34 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
--- a/src/HOL/Tools/lin_arith.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed May 05 18:25:34 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))
--- a/src/HOL/Tools/old_primrec.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/old_primrec.ML Wed May 05 18:25:34 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');
--- a/src/HOL/Tools/recfun_codegen.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Wed May 05 18:25:34 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;
--- a/src/HOL/Tools/refute.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/refute.ML Wed May 05 18:25:34 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))
--- a/src/HOL/Tools/sat_solver.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML Wed May 05 18:25:34 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 =
--- a/src/HOL/Tools/typedef_codegen.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/typedef_codegen.ML Wed May 05 18:25:34 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,
--- a/src/HOLCF/IOA/ABP/Check.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Check.ML Wed May 05 18:25:34 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
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Wed May 05 18:25:34 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);
--- a/src/HOLCF/Tools/Domain/domain_library.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Wed May 05 18:25:34 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
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Wed May 05 18:25:34 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
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed May 05 18:25:34 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))))
--- a/src/Provers/Arith/cancel_div_mod.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Wed May 05 18:25:34 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
--- a/src/Provers/Arith/fast_lin_arith.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed May 05 18:25:34 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)
--- a/src/Provers/order.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Provers/order.ML Wed May 05 18:25:34 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
--- a/src/Provers/trancl.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Provers/trancl.ML Wed May 05 18:25:34 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 (
--- a/src/Pure/ProofGeneral/pgip_input.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML Wed May 05 18:25:34 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 *)
--- a/src/Pure/library.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Pure/library.ML Wed May 05 18:25:34 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;
--- a/src/Tools/Metis/metis_env.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Tools/Metis/metis_env.ML Wed May 05 18:25:34 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;
--- a/src/Tools/WWW_Find/unicode_symbols.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Wed May 05 18:25:34 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;
--- a/src/ZF/Tools/datatype_package.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed May 05 18:25:34 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)
--- a/src/ZF/Tools/inductive_package.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed May 05 18:25:34 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: " ^