# HG changeset patch # User haftmann # Date 1256047981 -7200 # Node ID b22e44496dc2994ba764c34e5c552e794bebe05d # Parent 575bd6548df9d86244c1d9a2252ef22b8c31cb93 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions diff -r 575bd6548df9 -r b22e44496dc2 NEWS --- a/NEWS Tue Oct 20 13:37:56 2009 +0200 +++ b/NEWS Tue Oct 20 16:13:01 2009 +0200 @@ -213,6 +213,9 @@ *** ML *** +* Removed some old-style infix operations using polymorphic equality. +INCOMPATIBILITY. + * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML) provides a high-level programming interface to synchronized state variables with atomic update. This works via pure function diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Import/proof_kernel.ML Tue Oct 20 16:13:01 2009 +0200 @@ -281,9 +281,10 @@ | itr (a::rst) = i=a orelse itr rst in itr L end; +infix union; fun [] union S = S | S union [] = S - | (a::rst) union S2 = rst union (insert (op =) a S2) + | (a::rst) union S2 = rst union (insert (op =) a S2); fun implode_subst [] = [] | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest)) @@ -1229,7 +1230,7 @@ | add_consts (_, cs) = cs val t_consts = add_consts(t,[]) in - fn th => eq_set(t_consts,add_consts(prop_of th,[])) + fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, [])) end fun split_name str = diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Tue Oct 20 16:13:01 2009 +0200 @@ -563,7 +563,7 @@ let val th_consts = add_consts(prop_of th,[]) in - eq_set(t_consts,th_consts) + gen_eq_set (op =) (t_consts, th_consts) end end diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 16:13:01 2009 +0200 @@ -228,7 +228,7 @@ (case Symtab.lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a nominal datatype") | SOME dt => - if tnames' subset (map (#1 o snd) (#descr dt)) then + if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); @@ -251,7 +251,7 @@ val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) => map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns val _ = - (if forall (curry eq_set lsrs) lsrss andalso forall + (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) => forall (fn (_, (ls', _, rs', _, _)) => ls = ls' andalso rs = rs') eqns diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Set.thy Tue Oct 20 16:13:01 2009 +0200 @@ -303,7 +303,7 @@ fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso - ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) + gen_subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, [])) | check _ = false fun tr' (_ $ abs) = diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Oct 20 16:13:01 2009 +0200 @@ -489,7 +489,7 @@ val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname) in (case duplicates (op =) tvs of - [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx)) + [] => if gen_eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx)) else error ("Mutually recursive datatypes must have same type parameters") | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^ " : " ^ commas dups)) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 20 16:13:01 2009 +0200 @@ -257,7 +257,7 @@ fun get_nonrec_types descr sorts = map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) => Library.foldl (fn (Ts', (_, cargs)) => - filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr)); + gen_union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr)); (* get all recursive types in datatype description *) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Tue Oct 20 16:13:01 2009 +0200 @@ -90,7 +90,7 @@ IntGraph.empty |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => - if i = j orelse null (c1 inter t2) + if i = j orelse null (gen_inter (op =) (c1, t2)) then I else IntGraph.add_edge_acyclic (i,j)) num_branches num_branches end diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Function/pattern_split.ML Tue Oct 20 16:13:01 2009 +0200 @@ -101,7 +101,7 @@ let val t = Pattern.rewrite_term thy sigma [] feq1 in - fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t + fold_rev Logic.all (gen_inter (op =) (map Free (frees_in_term ctx t), vs')) t end in map instantiate substs diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 16:13:01 2009 +0200 @@ -348,7 +348,7 @@ | Add(lin1,lin2) => let val lis1 = resolve_proof vars lin1 val lis2 = resolve_proof vars lin2 - val dom = distinct (op =) ((map fst lis1) union (map fst lis2)) + val dom = distinct (op =) (gen_union (op =) (map fst lis1, map fst lis2)) in map (fn n => let val a = these (AList.lookup (op =) lis1 n) val b = these (AList.lookup (op =) lis2 n) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 16:13:01 2009 +0200 @@ -984,20 +984,20 @@ val dupTs = map snd (duplicates (op =) vTs) @ map_filter (AList.lookup (op =) vTs) vs; in - terms_vs (in_ts @ in_ts') subset vs andalso + gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso forall (is_eqT o fastype_of) in_ts' andalso - term_vs t subset vs andalso + gen_subset (op =) (term_vs t, vs) andalso forall is_eqT dupTs end) (modes_of_term modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) | Negprem (us, t) => find_first (fn Mode (_, is, _) => length us = length is andalso - terms_vs us subset vs andalso - term_vs t subset vs) + gen_subset (op =) (terms_vs us, vs) andalso + gen_subset (op =) (term_vs t, vs)) (modes_of_term modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) - | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) + | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], [])) else NONE ) ps); @@ -1047,16 +1047,16 @@ (if with_generator then (case select_mode_prem thy gen_modes' vs ps of SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) - (case p of Prem (us, _) => vs union terms_vs us | _ => vs) + (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs) (filter_out (equal p) ps) | _ => let val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length)) in case (find_first (fn generator_vs => is_some - (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of + (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) - (vs union generator_vs) ps + (gen_union (op =) (vs, generator_vs)) ps | NONE => let val _ = tracing ("ps:" ^ (commas (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps))) @@ -1065,7 +1065,7 @@ else NONE) | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) - (case p of Prem (us, _) => vs union terms_vs us | _ => vs) + (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs) (filter_out (equal p) ps)) val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts)); val in_vs = terms_vs in_ts; @@ -1073,13 +1073,13 @@ in if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso forall (is_eqT o fastype_of) in_ts' then - case check_mode_prems [] (param_vs union in_vs) ps of + case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of NONE => NONE | SOME (acc_ps, vs) => if with_generator then SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) else - if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE + if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE else NONE end; diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 16:13:01 2009 +0200 @@ -308,7 +308,7 @@ | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) | _ => (acc, dacc) val (cs,ds) = h ([],[]) p - val l = Integer.lcms (cs union ds) + val l = Integer.lcms (gen_union (op =) (cs, ds)) fun cv k ct = let val (tm as b$s$t) = term_of ct in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Tue Oct 20 16:13:01 2009 +0200 @@ -202,15 +202,15 @@ val dupTs = map snd (duplicates (op =) vTs) @ map_filter (AList.lookup (op =) vTs) vs; in - terms_vs (in_ts @ in_ts') subset vs andalso + gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso forall (is_eqT o fastype_of) in_ts' andalso - term_vs t subset vs andalso + gen_subset (op =) (term_vs t, vs) andalso forall is_eqT dupTs end) (if is_set then [Mode (([], []), [], [])] else modes_of modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) - | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) + | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], [])) else NONE) ps); fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) = @@ -222,7 +222,7 @@ | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of NONE => NONE | SOME (x, _) => check_mode_prems - (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs) + (case x of Prem (us, _, _) => gen_union (op =) (vs, terms_vs us) | _ => vs) (filter_out (equal x) ps)); val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts)); val in_vs = terms_vs in_ts; @@ -230,9 +230,9 @@ in forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso forall (is_eqT o fastype_of) in_ts' andalso - (case check_mode_prems (arg_vs union in_vs) ps of + (case check_mode_prems (gen_union (op =) (arg_vs, in_vs)) ps of NONE => false - | SOME vs => concl_vs subset vs) + | SOME vs => gen_subset (op =) (concl_vs, vs)) end; fun check_modes_pred thy arg_vs preds modes (p, ms) = @@ -482,7 +482,7 @@ fun constrain cs [] = [] | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of NONE => xs - | SOME xs' => xs inter xs') :: constrain cs ys; + | SOME xs' => gen_inter (op =) (xs, xs')) :: constrain cs ys; fun mk_extra_defs thy defs gr dep names module ts = Library.foldl (fn (gr, name) => diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/inductive_set.ML Tue Oct 20 16:13:01 2009 +0200 @@ -209,7 +209,7 @@ (case optf of NONE => fs | SOME f => AList.update op = (u, the_default f - (Option.map (curry op inter f) (AList.lookup op = fs u))) fs)); + (Option.map (curry (gen_inter (op =)) f) (AList.lookup op = fs u))) fs)); (**************************************************************) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Tue Oct 20 16:13:01 2009 +0200 @@ -631,7 +631,7 @@ let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith in {axioms = (mth, Meson.make_meta_clause ith) :: axioms, - tfrees = tfree_lits union tfrees} + tfrees = gen_union (op =) (tfree_lits, tfrees)} end; val lmap0 = List.foldl (add_thm true) {axioms = [], tfrees = init_tfrees ctxt} cls diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Tue Oct 20 16:13:01 2009 +0200 @@ -226,7 +226,7 @@ (case Symtab.lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a datatype") | SOME dt => - if tnames' subset (map (#1 o snd) (#descr dt)) then + if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/primrec.ML Tue Oct 20 16:13:01 2009 +0200 @@ -208,7 +208,7 @@ (case Symtab.lookup dt_info tname of NONE => primrec_error (quote tname ^ " is not a datatype") | SOME dt => - if tnames' subset (map (#1 o snd) (#descr dt)) then + if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/prop_logic.ML Tue Oct 20 16:13:01 2009 +0200 @@ -111,8 +111,8 @@ | indices False = [] | indices (BoolVar i) = [i] | indices (Not fm) = indices fm - | indices (Or (fm1, fm2)) = (indices fm1) union_int (indices fm2) - | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2); + | indices (Or (fm1, fm2)) = gen_union (op =) (indices fm1, indices fm2) + | indices (And (fm1, fm2)) = gen_union (op =) (indices fm1, indices fm2); (* ------------------------------------------------------------------------- *) (* maxidx: computes the maximal variable index occuring in a formula of *) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/record.ML Tue Oct 20 16:13:01 2009 +0200 @@ -1834,7 +1834,7 @@ val extN = full bname; val types = map snd fields; val alphas_fields = fold Term.add_tfree_namesT types []; - val alphas_ext = alphas inter alphas_fields; + val alphas_ext = gen_inter (op =) (alphas, alphas_fields); val len = length fields; val variants = Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/refute.ML Tue Oct 20 16:13:01 2009 +0200 @@ -1154,7 +1154,7 @@ val axioms = collect_axioms thy u (* Term.typ list *) val types = Library.foldl (fn (acc, t') => - acc union (ground_types thy t')) ([], u :: axioms) + gen_union (op =) (acc, (ground_types thy t'))) ([], u :: axioms) val _ = tracing ("Ground types: " ^ (if null types then "none." else commas (map (Syntax.string_of_typ_global thy) types))) @@ -2415,7 +2415,7 @@ (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) (* sanity check: typ_assoc must associate types to the *) (* elements of 'dtyps' (and only to those) *) - val _ = if not (Library.eq_set (dtyps, map fst typ_assoc)) + val _ = if not (gen_eq_set (op =) (dtyps, map fst typ_assoc)) then raise REFUTE ("IDT_recursion_interpreter", "type association has extra/missing elements") @@ -3007,7 +3007,7 @@ [Type ("fun", [T, Type ("bool", [])]), Type ("fun", [_, Type ("bool", [])])]), Type ("fun", [_, Type ("bool", [])])])) => - let nonfix union (* because "union" is used below *) + let val size_elem = size_of_type thy model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue Oct 20 16:13:01 2009 +0200 @@ -213,8 +213,9 @@ fun defs lhs rhs = let val (rator,args) = strip_comb lhs val ct = const_with_typ thy (dest_ConstFree rator) - in forall is_Var args andalso uni_mem gctypes ct andalso - Term.add_vars rhs [] subset Term.add_vars lhs [] + in + forall is_Var args andalso uni_mem gctypes ct andalso + gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) end handle ConstFree => false in diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Tue Oct 20 16:13:01 2009 +0200 @@ -93,7 +93,7 @@ val tconst_prefix = "tc_"; val class_prefix = "class_"; -fun union_all xss = List.foldl (op union) [] xss; +fun union_all xss = List.foldl (gen_union (op =)) [] xss; (*Provide readable names for the more common symbolic functions*) val const_trans_table = @@ -263,7 +263,7 @@ | pred_of_sort (LTFree (s,ty)) = (s,1) (*Given a list of sorted type variables, return a list of type literals.*) -fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts); +fun add_typs Ts = List.foldl (gen_union (op =)) [] (map sorts_on_typs Ts); (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a @@ -372,7 +372,7 @@ let val cpairs = type_class_pairs thy tycons classes val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses - in (classes' union classes, cpairs' union cpairs) end; + in (gen_union (op =) (classes', classes), gen_union (op =) (cpairs', cpairs)) end; fun make_arity_clauses_dfg dfg thy tycons classes = let val (classes', cpairs) = iter_type_class_pairs thy tycons classes diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Tue Oct 20 16:13:01 2009 +0200 @@ -154,7 +154,7 @@ | combterm_of dfg thy (P $ Q) = let val (P',tsP) = combterm_of dfg thy P val (Q',tsQ) = combterm_of dfg thy Q - in (CombApp(P',Q'), tsP union tsQ) end + in (CombApp(P',Q'), gen_union (op =) (tsP, tsQ)) end | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t); fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity) @@ -166,7 +166,7 @@ | literals_of_term1 dfg thy (lits,ts) P = let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) in - (Literal(pol,pred)::lits, ts union ts') + (Literal(pol,pred)::lits, gen_union (op =) (ts, ts')) end; fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; @@ -475,7 +475,7 @@ val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) - val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) + val tfree_clss = map RC.tptp_tfree_clause (List.foldl (gen_union (op =)) [] tfree_litss) val _ = File.write_list file ( map (#1 o (clause2tptp params)) axclauses @ diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Oct 20 16:13:01 2009 +0200 @@ -364,7 +364,7 @@ fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; fun replace_deps (old:int, new) (lno, t, deps) = - (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps)); + (lno, t, List.foldl (gen_union (op =)) [] (map (replace_dep (old, new)) deps)); (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ only in type information.*) diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/sat_solver.ML Tue Oct 20 16:13:01 2009 +0200 @@ -471,8 +471,8 @@ | forced_vars False = [] | forced_vars (BoolVar i) = [i] | forced_vars (Not (BoolVar i)) = [~i] - | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) - | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) + | forced_vars (Or (fm1, fm2)) = gen_inter (op =) (forced_vars fm1, forced_vars fm2) + | forced_vars (And (fm1, fm2)) = gen_union (op =) (forced_vars fm1, forced_vars fm2) (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) (* precedence, and the next partial evaluation of the formula returns 'False'. *) | forced_vars _ = error "formula is not in negation normal form" diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/transfer.ML Tue Oct 20 16:13:01 2009 +0200 @@ -143,7 +143,7 @@ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2, hints = subtract (op = : string*string -> bool) hints0 - (hints1 union_string hints2)} + (gen_union (op =) (hints1, hints2))} end; local @@ -151,7 +151,7 @@ in fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = - {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2} + {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = gen_union (op =) (hints1, hints2)} end; fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) = diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Tue Oct 20 16:13:01 2009 +0200 @@ -908,20 +908,20 @@ val dupTs = map snd (duplicates (op =) vTs) @ map_filter (AList.lookup (op =) vTs) vs; in - terms_vs (in_ts @ in_ts') subset vs andalso + gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso forall (is_eqT o fastype_of) in_ts' andalso - term_vs t subset vs andalso + gen_subset (op =) (term_vs t, vs) andalso forall is_eqT dupTs end) (modes_of_term modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) | Negprem (us, t) => find_first (fn Mode (_, is, _) => length us = length is andalso - terms_vs us subset vs andalso - term_vs t subset vs) + gen_subset (op =) (terms_vs us, vs) andalso + gen_subset (op =) (term_vs t, vs) (modes_of_term modes t handle Option => error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) - | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) + | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], [])) else NONE ) ps); @@ -964,22 +964,22 @@ (if with_generator then (case select_mode_prem thy gen_modes' vs ps of SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) - (case p of Prem (us, _) => vs union terms_vs us | _ => vs) + (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs) (filter_out (equal p) ps) | NONE => let val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length)) in case (find_first (fn generator_vs => is_some - (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of + (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) - (vs union generator_vs) ps + (gen_union (op =) (vs, generator_vs)) ps | NONE => NONE end) else NONE) | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) - (case p of Prem (us, _) => vs union terms_vs us | _ => vs) + (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs) (filter_out (equal p) ps)) val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts)); val in_vs = terms_vs in_ts; @@ -987,13 +987,13 @@ in if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso forall (is_eqT o fastype_of) in_ts' then - case check_mode_prems [] (param_vs union in_vs) ps of + case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of NONE => NONE | SOME (acc_ps, vs) => if with_generator then SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) else - if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE + if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE else NONE end; diff -r 575bd6548df9 -r b22e44496dc2 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 20 16:13:01 2009 +0200 @@ -59,8 +59,8 @@ fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of NONE => error ("Free type variable " ^ quote v ^ " on rhs.") - | SOME sort => if eq_set_string (s,defaultS) orelse - eq_set_string (s,sort ) + | SOME sort => if gen_eq_set (op =) (s, defaultS) orelse + gen_eq_set (op =) (s, sort) then TFree(v,sort) else error ("Inconsistent sort constraint" ^ " for type variable " ^ quote v)) diff -r 575bd6548df9 -r b22e44496dc2 src/Provers/Arith/cancel_div_mod.ML --- a/src/Provers/Arith/cancel_div_mod.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Provers/Arith/cancel_div_mod.ML Tue Oct 20 16:13:01 2009 +0200 @@ -74,7 +74,7 @@ fun proc ss t = let val (divs,mods) = coll_div_mod t ([],[]) in if null divs orelse null mods then NONE - else case divs inter mods of + else case gen_inter (op =) (divs, mods) of pq :: _ => SOME (cancel ss t pq) | [] => NONE end diff -r 575bd6548df9 -r b22e44496dc2 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 20 16:13:01 2009 +0200 @@ -385,7 +385,7 @@ let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in if not (null eqs) then let val c = - fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs [] + fold (fn Lineq(_,_,l,_) => fn cs => gen_union (op =) (l, cs)) eqs [] |> filter (fn i => i <> 0) |> sort (int_ord o pairself abs) |> hd diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/General/name_space.ML Tue Oct 20 16:13:01 2009 +0200 @@ -145,7 +145,7 @@ space |> add_name' name name |> fold (del_name name) - (if fully then names else names inter_string [Long_Name.base_name name]) + (if fully then names else gen_inter (op =) (names, [Long_Name.base_name name])) |> fold (del_name_extra name) (get_accesses space name) end; diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/General/ord_list.ML --- a/src/Pure/General/ord_list.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/General/ord_list.ML Tue Oct 20 16:13:01 2009 +0200 @@ -56,7 +56,6 @@ (* lists as sets *) -nonfix subset; fun subset ord (list1, list2) = let fun sub [] _ = true @@ -75,7 +74,6 @@ fun handle_same f x = f x handle SAME => x; (*union: insert elements of first list into second list*) -nonfix union; fun union ord list1 list2 = let fun unio [] _ = raise SAME @@ -88,7 +86,6 @@ in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end; (*intersection: filter second list for elements present in first list*) -nonfix inter; fun inter ord list1 list2 = let fun intr _ [] = raise SAME diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/General/path.ML Tue Oct 20 16:13:01 2009 +0200 @@ -42,7 +42,7 @@ | check_elem (chs as ["~"]) = err_elem "Illegal" chs | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs | check_elem chs = - (case ["/", "\\", "$", ":"] inter_string chs of + (case gen_inter (op =) (["/", "\\", "$", ":"], chs) of [] => chs | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Tue Oct 20 16:13:01 2009 +0200 @@ -289,7 +289,7 @@ val _ = message "Collecting constraints..."; val (t, prf, cs, env, _) = make_constraints_cprf thy (Envir.empty (maxidx_proof cprf ~1)) cprf'; - val cs' = map (fn p => (true, p, op union + val cs' = map (fn p => (true, p, gen_union (op =) (pairself (map (fst o dest_Var) o OldTerm.term_vars) p))) (map (pairself (Envir.norm_term env)) ((t, prop')::cs)); val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ..."); diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/ProofGeneral/pgip_parser.ML --- a/src/Pure/ProofGeneral/pgip_parser.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/ProofGeneral/pgip_parser.ML Tue Oct 20 16:13:01 2009 +0200 @@ -77,7 +77,7 @@ |> command K.prf_asm_goal goal |> command K.prf_script proofstep; -val _ = OuterKeyword.kinds subset_string Symtab.keys command_keywords +val _ = gen_subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords) orelse sys_error "Incomplete coverage of command keywords"; fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}] diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/Syntax/ast.ML Tue Oct 20 16:13:01 2009 +0200 @@ -104,7 +104,7 @@ val rvars = add_vars rhs []; in if has_duplicates (op =) lvars then SOME "duplicate vars in lhs" - else if not (rvars subset lvars) then SOME "rhs contains extra variables" + else if not (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables" else NONE end; diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/Syntax/parser.ML Tue Oct 20 16:13:01 2009 +0200 @@ -147,7 +147,7 @@ in if member (op =) nts l then (*update production's lookahead*) let - val new_lambda = is_none tk andalso nts subset lambdas; + val new_lambda = is_none tk andalso gen_subset (op =) (nts, lambdas); val new_tks = subtract (op =) l_starts ((if is_some tk then [the tk] else []) @ diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Tue Oct 20 16:13:01 2009 +0200 @@ -352,7 +352,7 @@ in SynExt { xprods = xprods, - consts = consts union_string mfix_consts, + consts = gen_union (op =) (consts, mfix_consts), prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns), parse_ast_translation = parse_ast_translation, parse_rules = parse_rules' @ parse_rules, diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue Oct 20 16:13:01 2009 +0200 @@ -227,7 +227,7 @@ fun check (t, NONE) = check (t, SOME (get_thm_names t)) | check ((_, thm), c as SOME thm_consts) = - (if pat_consts subset_string thm_consts andalso + (if gen_subset (op =) (pat_consts, thm_consts) andalso Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) then SOME (0, 0) else NONE, c); in check end; diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/codegen.ML Tue Oct 20 16:13:01 2009 +0200 @@ -599,8 +599,8 @@ else Pretty.block (separate (Pretty.brk 1) (p :: ps)); fun new_names t xs = Name.variant_list - (map (fst o fst o dest_Var) (OldTerm.term_vars t) union - OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs); + (gen_union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t), + OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs); fun new_name t x = hd (new_names t [x]); diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/library.ML --- a/src/Pure/library.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/library.ML Tue Oct 20 16:13:01 2009 +0200 @@ -11,8 +11,7 @@ infix 2 ? infix 3 o oo ooo oooo infix 4 ~~ upto downto -infix orf andf \ \\ mem mem_int mem_string union union_int - union_string inter inter_int inter_string subset subset_int subset_string +infix orf andf \ \\ mem mem_int mem_string signature BASIC_LIBRARY = sig @@ -163,19 +162,8 @@ val mem: ''a * ''a list -> bool val mem_int: int * int list -> bool val mem_string: string * string list -> bool - val union: ''a list * ''a list -> ''a list - val union_int: int list * int list -> int list - val union_string: string list * string list -> string list val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list - val inter: ''a list * ''a list -> ''a list - val inter_int: int list * int list -> int list - val inter_string: string list * string list -> string list - val subset: ''a list * ''a list -> bool - val subset_int: int list * int list -> bool - val subset_string: string list * string list -> bool - val eq_set: ''a list * ''a list -> bool - val eq_set_string: string list * string list -> bool val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool val \ : ''a list * ''a -> ''a list @@ -811,70 +799,20 @@ fun (x: string) mem_string xs = member (op =) xs x; (*union of sets represented as lists: no repetitions*) -fun xs union [] = xs - | [] union ys = ys - | (x :: xs) union ys = xs union (insert (op =) x ys); - -(*union of sets, optimized version for ints*) -fun (xs:int list) union_int [] = xs - | [] union_int ys = ys - | (x :: xs) union_int ys = xs union_int (insert (op =) x ys); - -(*union of sets, optimized version for strings*) -fun (xs:string list) union_string [] = xs - | [] union_string ys = ys - | (x :: xs) union_string ys = xs union_string (insert (op =) x ys); - -(*generalized union*) fun gen_union eq (xs, []) = xs | gen_union eq ([], ys) = ys | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys); - (*intersection*) -fun [] inter ys = [] - | (x :: xs) inter ys = - if x mem ys then x :: (xs inter ys) else xs inter ys; - -(*intersection, optimized version for ints*) -fun ([]:int list) inter_int ys = [] - | (x :: xs) inter_int ys = - if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys; - -(*intersection, optimized version for strings *) -fun ([]:string list) inter_string ys = [] - | (x :: xs) inter_string ys = - if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys; - -(*generalized intersection*) fun gen_inter eq ([], ys) = [] | gen_inter eq (x::xs, ys) = if member eq ys x then x :: gen_inter eq (xs, ys) else gen_inter eq (xs, ys); - (*subset*) -fun [] subset ys = true - | (x :: xs) subset ys = x mem ys andalso xs subset ys; - -(*subset, optimized version for ints*) -fun ([]: int list) subset_int ys = true - | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys; - -(*subset, optimized version for strings*) -fun ([]: string list) subset_string ys = true - | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys; +fun gen_subset eq (xs, ys) = forall (member eq ys) xs; (*set equality*) -fun eq_set (xs, ys) = - xs = ys orelse (xs subset ys andalso ys subset xs); - -(*set equality for strings*) -fun eq_set_string ((xs: string list), ys) = - xs = ys orelse (xs subset_string ys andalso ys subset_string xs); - -fun gen_subset eq (xs, ys) = forall (member eq ys) xs; - fun gen_eq_set eq (xs, ys) = eq_list eq (xs, ys) orelse (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs)); diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/meta_simplifier.ML Tue Oct 20 16:13:01 2009 +0200 @@ -864,7 +864,7 @@ while the premises are solved.*) fun cond_skel (args as (_, (lhs, rhs))) = - if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args + if gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args else skel0; (* diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/pattern.ML Tue Oct 20 16:13:01 2009 +0200 @@ -216,10 +216,10 @@ fun flexflex2(env,binders,F,Fty,is,G,Gty,js) = let fun ff(F,Fty,is,G as (a,_),Gty,js) = - if js subset_int is + if gen_subset (op =) (js, is) then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js)) in Envir.update (((F, Fty), t), env) end - else let val ks = is inter_int js + else let val ks = gen_inter (op =) (is, js) val Hty = type_of_G env (Fty,length is,map (idx is) ks) val (env',H) = Envir.genvar a (env,Hty) fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); @@ -339,7 +339,7 @@ let val js = loose_bnos t in if null is then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH - else if js subset_int is + else if gen_subset (op =) (js, is) then let val t' = if downto0(is,length binders - 1) then t else mapbnd (idx is) t in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/proofterm.ML Tue Oct 20 16:13:01 2009 +0200 @@ -900,8 +900,8 @@ fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then - vs union map_filter (fn Var (ixn, T) => - if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t) + gen_union (op =) (vs, map_filter (fn Var (ixn, T) => + if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs; fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) = @@ -918,7 +918,7 @@ | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); -fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q +fun prop_vars (Const ("==>", _) $ P $ Q) = gen_union (op =) (prop_vars P, prop_vars Q) | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []); @@ -936,9 +936,9 @@ end; fun needed_vars prop = - Library.foldl (op union) - ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union - prop_vars prop; + gen_union (op =) (Library.foldl (gen_union (op =)) + ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))), + prop_vars prop); fun gen_axm_proof c name prop = let @@ -975,7 +975,7 @@ let val p as (_, is', ch', prf') = shrink ls lev prf2; val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1 - in (is union is', ch orelse ch', ts', + in (gen_union (op =) (is, is'), ch orelse ch', ts', if ch orelse ch' then prf'' %% prf' else prf) end | shrink' ls lev ts prfs (prf as prf1 % t) = @@ -1004,15 +1004,15 @@ val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => insert (op =) ixn (case AList.lookup (op =) insts ixn of - SOME (SOME t) => if is_proj t then ixns union ixns' else ixns' - | _ => ixns union ixns')) + SOME (SOME t) => if is_proj t then gen_union (op =) (ixns, ixns') else ixns' + | _ => gen_union (op =) (ixns, ixns'))) (needed prop ts'' prfs, add_npvars false true [] ([], prop)); val insts' = map (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE) | (_, x) => (false, x)) insts in ([], false, insts' @ map (pair false) ts'', prf) end and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) = - (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs + gen_union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs) | needed (Var (ixn, _)) (_::_) _ = [ixn] | needed _ _ _ = []; in shrink end; diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/sorts.ML Tue Oct 20 16:13:01 2009 +0200 @@ -72,8 +72,8 @@ (** ordered lists of sorts **) val make = OrdList.make TermOrd.sort_ord; -val op subset = OrdList.subset TermOrd.sort_ord; -val op union = OrdList.union TermOrd.sort_ord; +val subset = OrdList.subset TermOrd.sort_ord; +val union = OrdList.union TermOrd.sort_ord; val subtract = OrdList.subtract TermOrd.sort_ord; val remove_sort = OrdList.remove TermOrd.sort_ord; diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/thm.ML Tue Oct 20 16:13:01 2009 +0200 @@ -1463,7 +1463,7 @@ (case duplicates (op =) cs of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state) | [] => - (case cs inter_string freenames of + (case gen_inter (op =) (cs, freenames) of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) | [] => Thm (der, diff -r 575bd6548df9 -r b22e44496dc2 src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Pure/variable.ML Tue Oct 20 16:13:01 2009 +0200 @@ -301,7 +301,7 @@ val names = names_of ctxt; val (xs', names') = if is_body ctxt then Name.variants xs names |>> map Name.skolem - else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); + else (no_dups (gen_inter (op =) (xs, ys)); no_dups (gen_inter (op =) (xs, zs)); (xs, fold Name.declare xs names)); in ctxt |> new_fixes names' xs xs' end; diff -r 575bd6548df9 -r b22e44496dc2 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Tue Oct 20 16:13:01 2009 +0200 @@ -139,13 +139,13 @@ val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds); val (conds_tyvs,cond_vs) = Library.foldl (fn ((tyvs, vs), t) => - (Library.union + (gen_union (op =) (OldTerm.term_tvars t, tyvs), - Library.union + gen_union (op =) (map Term.dest_Var (OldTerm.term_vars t), vs))) (([],[]), rule_conds); val termvars = map Term.dest_Var (OldTerm.term_vars tgt); - val vars_to_fix = Library.union (termvars, cond_vs); + val vars_to_fix = gen_union (op =) (termvars, cond_vs); val (renamings, names2) = List.foldr (fn (((n,i),ty), (vs, names')) => let val n' = Name.variant names' n in diff -r 575bd6548df9 -r b22e44496dc2 src/Tools/Metis/metis_env.ML --- a/src/Tools/Metis/metis_env.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Tools/Metis/metis_env.ML Tue Oct 20 16:13:01 2009 +0200 @@ -1,5 +1,5 @@ (* Metis-specific ML environment *) -nonfix ++ -- RL mem union subset; +nonfix ++ -- RL mem; val explode = String.explode; val implode = String.implode; val print = TextIO.print; diff -r 575bd6548df9 -r b22e44496dc2 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/ZF/Tools/primrec_package.ML Tue Oct 20 16:13:01 2009 +0200 @@ -65,7 +65,7 @@ in if has_duplicates (op =) lfrees then raise RecError "repeated variable name in pattern" - else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then + else if not (gen_subset (op =) (Term.add_frees rhs [], lfrees)) then raise RecError "extra variables on rhs" else if length middle > 1 then raise RecError "more than one non-variable in pattern"