--- a/src/Provers/IsaPlanner/rw_inst.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Provers/IsaPlanner/rw_inst.ML Thu Sep 21 19:04:20 2006 +0200
@@ -179,7 +179,7 @@
Term.add_term_tfrees (t,tfrees)))
([],[]) ts;
val unfixed_tvars =
- List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
+ List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
in (fixtyinsts, tfrees) end;
--- a/src/Provers/blast.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Provers/blast.ML Thu Sep 21 19:04:20 2006 +0200
@@ -293,7 +293,7 @@
| Abs (a,body) => (*eta-contract if possible*)
(case wkNormAux body of
nb as (f $ t) =>
- if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
+ if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0
then Abs(a,nb)
else wkNorm (incr_boundvars ~1 f)
| nb => Abs (a,nb))
@@ -385,7 +385,7 @@
| from (Term.Abs (a,_,u)) =
(case from u of
u' as (f $ Bound 0) =>
- if (0 mem_int loose_bnos f) then Abs(a,u')
+ if member (op =) (loose_bnos f) 0 then Abs(a,u')
else incr_boundvars ~1 f
| u' => Abs(a,u'))
| from (Term.$ (f,u)) = from f $ from u
@@ -679,7 +679,7 @@
(*Eta-contract a term from outside: just enough to reduce it to an atom*)
fun eta_contract_atom (t0 as Abs(a, body)) =
(case eta_contract2 body of
- f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
+ f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0
else eta_contract_atom (incr_boundvars ~1 f)
| _ => t0)
| eta_contract_atom t = t
@@ -1178,8 +1178,8 @@
(*List of variables not appearing as arguments to the given parameter*)
fun getVars [] i = []
- | getVars ((_,(v,is))::alist) i =
- if i mem is then getVars alist i
+ | getVars ((_,(v,is))::alist) (i: int) =
+ if member (op =) is i then getVars alist i
else v :: getVars alist i;
exception TRANS of string;
--- a/src/Provers/splitter.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Provers/splitter.ML Thu Sep 21 19:04:20 2006 +0200
@@ -165,7 +165,7 @@
has a body of type T; otherwise the expansion thm will fail later on
*)
fun type_test (T,lbnos,apsns) =
- let val (_,U,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
+ let val (_,U: typ,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
in T=U end;
(*************************************************************************
@@ -196,7 +196,7 @@
lifting is required before applying the split-theorem.
******************************************************************************)
-fun mk_split_pack (thm, T, T', n, ts, apsns, pos, TB, t) =
+fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) =
if n > length ts then []
else let val lev = length apsns
val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
@@ -398,9 +398,8 @@
| split_asm_tac splits =
let val cname_list = map (fst o fst o split_thm_info) splits;
- fun is_case (a,_) = a mem cname_list;
fun tac (t,i) =
- let val n = find_index (exists_Const is_case)
+ let val n = find_index (exists_Const (member (op =) cname_list o #1))
(Logic.strip_assums_hyp t);
fun first_prem_is_disj (Const ("==>", _) $ (Const (c, _)
$ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or
--- a/src/Pure/General/output.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/General/output.ML Thu Sep 21 19:04:20 2006 +0200
@@ -67,7 +67,7 @@
val print_mode = ref ([]: string list);
-fun has_mode s = s mem_string ! print_mode;
+fun has_mode s = member (op =) (! print_mode) s;
type mode_fns =
{output: string -> string * real,
--- a/src/Pure/Isar/args.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Isar/args.ML Thu Sep 21 19:04:20 2006 +0200
@@ -349,10 +349,10 @@
local
-val exclude = explode "()[],";
+val exclude = member (op =) (explode "()[],");
fun atomic blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
- k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ","));
+ k <> Keyword orelse not (exclude x) orelse blk andalso x = ","));
fun args blk x = Scan.optional (args1 blk) [] x
and args1 blk x =
--- a/src/Pure/Isar/locale.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Isar/locale.ML Thu Sep 21 19:04:20 2006 +0200
@@ -1644,7 +1644,7 @@
val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
val env = Term.add_term_free_names (body, []);
- val xs = filter (fn (x, _) => x mem_string env) parms;
+ val xs = filter (member (op =) env o #1) parms;
val Ts = map #2 xs;
val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
|> Library.sort_wrt #1 |> map TFree;
--- a/src/Pure/Isar/outer_lex.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Isar/outer_lex.ML Thu Sep 21 19:04:20 2006 +0200
@@ -190,8 +190,7 @@
(* scan symbolic idents *)
-val sym_chars = explode "!#$%&*+-/<=>?@^_|~";
-fun is_sym_char s = s mem sym_chars;
+val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
val scan_symid =
Scan.any1 is_sym_char >> implode ||
--- a/src/Pure/Isar/session.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Isar/session.ML Thu Sep 21 19:04:20 2006 +0200
@@ -50,7 +50,7 @@
(* init *)
fun init reset parent name =
- if not (parent mem_string (! session)) orelse not (! session_finished) then
+ if not (member (op =) (! session) parent) orelse not (! session_finished) then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else (add_path reset name; session_finished := false);
--- a/src/Pure/Isar/toplevel.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Sep 21 19:04:20 2006 +0200
@@ -619,7 +619,7 @@
|> (if ! profiling > 0 then do_profiling else I)
|> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
val _ = conditional (int andalso not (! quiet) andalso
- exists (fn m => m mem_string print) ("" :: ! print_mode))
+ exists (member (op =) print) ("" :: ! print_mode))
(fn () => print_state false result);
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
--- a/src/Pure/Proof/extraction.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Sep 21 19:04:20 2006 +0200
@@ -54,10 +54,10 @@
fun typeof_proc defaultS vs (Const ("typeof", _) $ u) =
SOME (mk_typ (case strip_comb u of
(Var ((a, i), _), _) =>
- if a mem vs then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS)
+ if member (op =) vs a then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS)
else nullT
| (Free (a, _), _) =>
- if a mem vs then TFree ("'" ^ a, defaultS) else nullT
+ if member (op =) vs a then TFree ("'" ^ a, defaultS) else nullT
| _ => nullT))
| typeof_proc _ _ _ = NONE;
@@ -147,7 +147,7 @@
fun relevant_vars types prop = foldr (fn
(Var ((a, i), T), vs) => (case strip_type T of
- (_, Type (s, _)) => if s mem types then a :: vs else vs
+ (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
| _ => vs)
| (_, vs) => vs) [] (vars_of prop);
@@ -320,7 +320,7 @@
(map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
val vars = vars_of prop;
val vars' = filter_out (fn v =>
- tname_of (body_type (fastype_of v)) mem rtypes) vars;
+ member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
val T = etype_of thy' vs [] prop;
val (T', thw) = Type.freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
@@ -474,7 +474,7 @@
val n = Int.min (length vars, length ts);
fun add_args ((Var ((a, i), _), t), (vs', tye)) =
- if a mem rvs then
+ if member (op =) rvs a then
let val T = etype_of thy' vs Ts t
in if T = nullT then (vs', tye)
else (a :: vs', (("'" ^ a, i), T) :: tye)
@@ -483,7 +483,7 @@
in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
- fun find vs = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
+ fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
fun find' s = map snd o List.filter (equal s o fst)
fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
@@ -523,9 +523,9 @@
let
val (Us, T) = strip_type (fastype_of1 (Ts, t));
val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
- (if tname_of T mem rtypes then t'
+ (if member (op =) rtypes (tname_of T) then t'
else (case t' of SOME (u $ _) => SOME u | _ => NONE));
- val u = if not (tname_of T mem rtypes) then t else
+ val u = if not (member (op =) rtypes (tname_of T)) then t else
let
val eT = etype_of thy' vs Ts t;
val (r, Us') = if eT = nullT then (nullt, Us) else
@@ -628,7 +628,7 @@
| extr d defs vs ts Ts hs (prf % SOME t) =
let val (defs', u) = extr d defs vs (t :: ts) Ts hs prf
in (defs',
- if tname_of (body_type (fastype_of1 (Ts, t))) mem rtypes then u
+ if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
else u $ t)
end
@@ -661,8 +661,8 @@
corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
val nt = Envir.beta_norm t;
- val args = filter_out (fn v => tname_of (body_type
- (fastype_of v)) mem rtypes) (vfs_of prop);
+ val args = filter_out (fn v => member (op =) rtypes
+ (tname_of (body_type (fastype_of v)))) (vfs_of prop);
val args' = List.filter (fn v => Logic.occs (v, nt)) args;
val t' = mkabs nt args';
val T = fastype_of t';
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Sep 21 19:04:20 2006 +0200
@@ -223,7 +223,7 @@
AbsP (s, t, insert_refl defs Ts prf)
| insert_refl defs Ts prf = (case strip_combt prf of
(PThm ((s, _), _, prop, SOME Ts), ts) =>
- if s mem defs then
+ if member (op =) defs s then
let
val vs = vars_of prop;
val tvars = term_tvars prop;
@@ -246,7 +246,7 @@
let
val cnames = map (fst o dest_Const o fst) defs';
val thms = maps (fn (s, ps) =>
- if s mem defnames then []
+ if member (op =) defnames s then []
else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
null (term_consts p inter cnames)) ps))
(Symtab.dest (thms_of_proof prf Symtab.empty))
--- a/src/Pure/Syntax/lexicon.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Sep 21 19:04:20 2006 +0200
@@ -145,8 +145,7 @@
val tvarT = Type ("tvar", []);
val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
-
-fun is_terminal s = s mem terminals;
+val is_terminal = member (op =) terminals;
(* str_of_token *)
--- a/src/Pure/Syntax/parser.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Sep 21 19:04:20 2006 +0200
@@ -75,7 +75,7 @@
(*store chain if it does not already exist*)
val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
let val old_tos = these (AList.lookup (op =) chains from) in
- if lhs mem old_tos then (NONE, chains)
+ if member (op =) old_tos lhs then (NONE, chains)
else (SOME from, AList.update (op =) (from, lhs ins old_tos) chains)
end;
@@ -101,13 +101,13 @@
val tos = connected_with chains' [lhs] [lhs];
in (copy_lookahead tos [],
- (if lhs mem lambdas then tos else []) union lambdas)
+ (if member (op =) lambdas lhs then tos else []) union lambdas)
end;
(*test if new production can produce lambda
(rhs must either be empty or only consist of lambda NTs)*)
val (new_lambda, lambdas') =
- if forall (fn (Nonterminal (id, _)) => id mem lambdas'
+ if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
| (Terminal _) => false) rhs then
(true, lambdas' union (connected_with chains' [lhs] [lhs]))
else
@@ -118,7 +118,7 @@
fun lookahead_dependency _ [] nts = (NONE, nts)
| lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts)
| lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts =
- if nt mem lambdas then
+ if member (op =) lambdas nt then
lookahead_dependency lambdas symbs (nt :: nts)
else (NONE, nt :: nts);
@@ -145,7 +145,7 @@
nt_dependencies added_tks nt_prods =
let val (tk, nts) = lookahead_dependency lambdas rhs [];
in
- if l mem nts then (*update production's lookahead*)
+ if member (op =) nts l then (*update production's lookahead*)
let
val new_lambda = is_none tk andalso nts subset lambdas;
@@ -248,7 +248,7 @@
fun add_nts [] = ()
| add_nts (nt :: nts) =
let val ((old_nts, old_tks), ps) = Array.sub (prods, nt);
- in if lhs mem old_nts then ()
+ in if member (op =) old_nts lhs then ()
else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
end;
@@ -273,7 +273,7 @@
grammar does not contain new production already*)
val (tk_prods', is_new') =
if is_some prod_count then
- if new_prod mem tk_prods then (tk_prods, false)
+ if member (op =) tk_prods new_prod then (tk_prods, false)
else (new_prod :: tk_prods, true)
else (new_prod :: tk_prods, true);
@@ -304,7 +304,7 @@
(*token under which old productions which
depend on changed_nt could be stored*)
val key =
- case find_first (fn t => not (t mem new_tks))
+ case find_first (not o member (op =) new_tks)
(starts_for_nt changed_nt) of
NONE => SOME UnknownStart
| t => t;
@@ -320,13 +320,13 @@
val (tk, depends) = lookahead_dependency lambdas' rhs [];
(*test if this production has to be copied*)
- val update = changed_nt mem depends;
+ val update = member (op =) depends changed_nt;
(*test if production could already be associated with
a member of new_tks*)
val lambda = length depends > 1 orelse
not (null depends) andalso is_some tk
- andalso the tk mem new_tks;
+ andalso member (op =) new_tks (the tk);
(*associate production with new starting tokens*)
fun copy [] nt_prods = nt_prods
@@ -811,7 +811,7 @@
else false
| reduction tk minPrec checked
(Nonterminal (nt, nt_prec) :: _, _, prec) =
- if prec >= minPrec andalso not (nt mem checked) then
+ if prec >= minPrec andalso not (member (op =) checked nt) then
let val chained = connected_with chains [nt] [nt];
in exists
(reduction tk nt_prec (chained @ checked))
--- a/src/Pure/Syntax/syntax.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Sep 21 19:04:20 2006 +0200
@@ -462,7 +462,7 @@
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
- if x mem consts orelse NameSpace.is_qualified x then Ast.Constant x
+ if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x
else ast
| constify (Ast.Appl asts) = Ast.Appl (map constify asts);
in
--- a/src/Pure/Thy/present.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Thy/present.ML Thu Sep 21 19:04:20 2006 +0200
@@ -88,7 +88,7 @@
val _ = Context.add_setup BrowserInfoData.init;
fun get_info thy =
- if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
+ if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
then {name = Context.PureN, session = [], is_local = false}
else BrowserInfoData.get thy;
@@ -541,7 +541,7 @@
fun known name =
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
- in fn s => s mem_string ss end;
+ in member (op =) ss end;
val known_syms = known "syms.lst";
val known_ctrls = known "ctrls.lst";
--- a/src/Pure/Thy/thm_deps.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Thy/thm_deps.ML Thu Sep 21 19:04:20 2006 +0200
@@ -54,7 +54,7 @@
| NONE => [])
| _ => ["global"]);
in
- if name mem parents' then (gra', parents union parents')
+ if member (op =) parents' name then (gra', parents union parents')
else (Symtab.update (name,
{name = Sign.base_name name, ID = name,
dir = space_implode "/" (session @ prefx),
--- a/src/Pure/Thy/thy_info.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Sep 21 19:04:20 2006 +0200
@@ -352,8 +352,8 @@
val path = Path.expand (Path.unpack str);
val name = Path.pack (Path.base path);
in
- if name mem_string initiators then error (cycle_msg initiators) else ();
- if known_thy name andalso is_finished name orelse name mem_string visited then
+ if member (op =) initiators name then error (cycle_msg initiators) else ();
+ if known_thy name andalso is_finished name orelse member (op =) visited name then
(visited, (true, name))
else
let
--- a/src/Pure/proof_general.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/proof_general.ML Thu Sep 21 19:04:20 2006 +0200
@@ -867,7 +867,7 @@
and even if we did, we'd have to mess around here a whole lot more first
to pick out the terms from the syntax. *)
- if (name mem plain_items) then plain_item
+ if member (op =) plain_items name then plain_item
else case name of
"text" => comment_item
| "text_raw" => comment_item
@@ -1460,9 +1460,9 @@
local
-val regexp_meta = explode ".*+?[]^$";
+val regexp_meta = member (op =) (explode ".*+?[]^$");
val regexp_quote =
- implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode;
+ implode o map (fn c => if regexp_meta c then "\\\\" ^ c else c) o explode;
fun defconst name strs =
"\n(defconst isar-keywords-" ^ name ^
--- a/src/Pure/pure_thy.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/pure_thy.ML Thu Sep 21 19:04:20 2006 +0200
@@ -108,7 +108,7 @@
fun map_tags f thm =
Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
-fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
+fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]);
fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s'));
fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
--- a/src/Pure/sign.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/sign.ML Thu Sep 21 19:04:20 2006 +0200
@@ -278,7 +278,7 @@
fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
val typ_match = Type.typ_match o tsig_of;
val typ_unify = Type.unify o tsig_of;
-fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
+val is_logtype = member (op =) o Type.logical_types o tsig_of;
(* polymorphic constants *)
@@ -338,7 +338,7 @@
fun mapping add_names f t =
let
- fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
+ fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
val tab = map_filter f' (add_names t []);
fun get x = the_default x (AList.lookup (op =) tab x);
in get end;
@@ -663,7 +663,7 @@
fun add_typedecls decls thy =
let
- fun type_of (a, vs, mx) =
+ fun type_of (a, vs: string list, mx) =
if not (has_duplicates (op =) vs) then (a, length vs, mx)
else error ("Duplicate parameters in type declaration: " ^ quote a);
in add_types (map type_of decls) thy end;
--- a/src/Pure/tctical.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/tctical.ML Thu Sep 21 19:04:20 2006 +0200
@@ -432,7 +432,7 @@
fun swap_ctpair (t,u) = (cterm u, cterm t)
(*Subgoal variables: make Free; lift type over params*)
fun mk_subgoal_inst concl_vars (var as Var(v,T)) =
- if var mem concl_vars
+ if member (op =) concl_vars var
then (var, true, free_of "METAHYP2_" (v,T))
else (var, false,
free_of "METAHYP2_" (v, map #2 params --->T))
--- a/src/Pure/term.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/term.ML Thu Sep 21 19:04:20 2006 +0200
@@ -964,7 +964,7 @@
fun is_first_order quants =
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
| first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
- q mem_string quants andalso (*it is a known quantifier*)
+ member (op =) quants q andalso (*it is a known quantifier*)
not (is_funtype T) andalso first_order1 (T::Ts) body
| first_order1 Ts t =
case strip_comb t of
--- a/src/Pure/unify.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/unify.ML Thu Sep 21 19:04:20 2006 +0200
@@ -426,7 +426,7 @@
let val (head,args) = strip_comb t
in
case head of
- Bound i => (i-lev) mem_int banned orelse
+ Bound i => member (op =) banned (i-lev) orelse
exists (rigid_bound (lev, banned)) args
| Var _ => false (*no rigid occurrences here!*)
| Abs (_,_,u) =>
@@ -439,7 +439,7 @@
fun change_bnos banned =
let fun change lev (Bound i) =
if i<lev then Bound i
- else if (i-lev) mem_int banned
+ else if member (op =) banned (i-lev)
then raise CHANGE_FAIL (**flexible occurrence: give up**)
else Bound (i - length (List.filter (fn j => j < i-lev) banned))
| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
@@ -500,7 +500,7 @@
fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
let val loot = loose_bnos t and loou = loose_bnos u
fun add_index (((a,T), j), (bnos, newbinder)) =
- if j mem_int loot andalso j mem_int loou
+ if member (op =) loot j andalso member (op =) loou j
then (bnos, (a,T)::newbinder) (*needed by both: keep*)
else (j::bnos, newbinder); (*remove*)
val indices = 0 upto (length rbinder - 1);