# HG changeset patch # User wenzelm # Date 1158858260 -7200 # Node ID ffbc5a57191a2dcd3c4d2f76e593fea8b45cb233 # Parent 2024d9f7df9cf6fb27420c48919081608c006ebc member (op =); diff -r 2024d9f7df9c -r ffbc5a57191a src/Provers/IsaPlanner/rw_inst.ML --- 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; diff -r 2024d9f7df9c -r ffbc5a57191a src/Provers/blast.ML --- 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; diff -r 2024d9f7df9c -r ffbc5a57191a src/Provers/splitter.ML --- 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 diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/General/output.ML --- 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, diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Isar/args.ML --- 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 = diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Isar/locale.ML --- 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; diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Isar/outer_lex.ML --- 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 || diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Isar/session.ML --- 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); diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Isar/toplevel.ML --- 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; diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Proof/extraction.ML --- 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'; diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Proof/proof_rewrite_rules.ML --- 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)) diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Syntax/lexicon.ML --- 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 *) diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Syntax/parser.ML --- 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)) diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Syntax/syntax.ML --- 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 diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Thy/present.ML --- 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"; diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Thy/thm_deps.ML --- 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), diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/Thy/thy_info.ML --- 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 diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/proof_general.ML --- 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 ^ diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/pure_thy.ML --- 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; diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/sign.ML --- 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; diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/tctical.ML --- 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)) diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/term.ML --- 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 diff -r 2024d9f7df9c -r ffbc5a57191a src/Pure/unify.ML --- 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 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);