# HG changeset patch # User haftmann # Date 1256119376 -7200 # Node ID ddf1f03a9ad9a01c0c17843a4a48d28095da2f36 # Parent 6793b02a3409c02a90622c8cafcd44c24b87fa26 curried union as canonical list operation diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Wed Oct 21 12:02:56 2009 +0200 @@ -165,7 +165,7 @@ val empty = [] val copy = I val extend = I - fun merge _ = Library.union Thm.eq_thm + fun merge _ = Library.merge Thm.eq_thm_prop ) val hol4_debug = Unsynchronized.ref false diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Wed Oct 21 12:02:56 2009 +0200 @@ -78,7 +78,7 @@ val empty = [] val copy = I val extend = I - fun merge _ = Library.union Thm.eq_thm + fun merge _ = Library.merge Thm.eq_thm_prop ) fun print_shuffles thy = diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 12:02:56 2009 +0200 @@ -244,7 +244,7 @@ fun monomial_lcm m1 m2 = fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2))) - (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty); + (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1) (FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty); fun monomial_multidegree m = FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;; @@ -314,7 +314,7 @@ FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0; fun poly_variables p = - sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);; + sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);; (* Order monomials for human presentation. *) @@ -1059,8 +1059,8 @@ fun real_positivnullstellensatz_general prover linf d eqs leqs pol = let - val vars = fold_rev (curry (union (op aconvc)) o poly_variables) - (pol::eqs @ map fst leqs) [] + val vars = fold_rev (union (op aconvc) o poly_variables) + (pol :: eqs @ map fst leqs) [] val monoid = if linf then (poly_const rat_1,RealArith.Rational_lt rat_1):: (filter (fn (p,c) => multidegree p <= d) leqs) diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Library/normarith.ML Wed Oct 21 12:02:56 2009 +0200 @@ -286,7 +286,7 @@ val dests = distinct (op aconvc) (map snd rawdests) val srcfuns = map vector_lincomb sources val destfuns = map vector_lincomb dests - val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] + val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] val n = length srcfuns val nvs = 1 upto n val srccombs = srcfuns ~~ nvs diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Wed Oct 21 12:02:56 2009 +0200 @@ -620,7 +620,7 @@ | NONE => (case eqs of [] => let val vars = remove (op aconvc) one_tm - (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) + (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) in linear_ineqs vars (les,lts) end | (e,p)::es => if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else @@ -679,7 +679,7 @@ val le_pols = map rhs le val lt_pols = map rhs lt val aliens = filter is_alien - (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) + (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (eq_pols @ le_pols @ lt_pols) []) val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols) diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/SEQ.thy Wed Oct 21 12:02:56 2009 +0200 @@ -1089,10 +1089,10 @@ subsubsection {* Cauchy Sequences are Convergent *} -axclass complete_space \ metric_space - Cauchy_convergent: "Cauchy X \ convergent X" +class complete_space = + assumes Cauchy_convergent: "Cauchy X \ convergent X" -axclass banach \ real_normed_vector, complete_space +class banach = real_normed_vector + complete_space theorem LIMSEQ_imp_Cauchy: assumes X: "X ----> a" shows "Cauchy X" diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Oct 21 12:02:56 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)) => - union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr)); + union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr)); (* get all recursive types in datatype description *) diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:02:56 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 =) (union (op =) (map fst lis1, map fst lis2)) + val dom = distinct (op =) (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 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 12:02:56 2009 +0200 @@ -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, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => 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' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of + (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) - (union (op =) (vs, generator_vs)) ps + (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, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => 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,7 +1073,7 @@ 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 [] (union (op =) (param_vs, in_vs)) ps of + case check_mode_prems [] (union (op =) param_vs in_vs) ps of NONE => NONE | SOME (acc_ps, vs) => if with_generator then diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 12:02:56 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 (union (op =) (cs, ds)) + val l = Integer.lcms (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 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/TFL/post.ML Wed Oct 21 12:02:56 2009 +0200 @@ -28,7 +28,7 @@ *--------------------------------------------------------------------------*) fun termination_goals rules = map (Type.freeze o HOLogic.dest_Trueprop) - (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules); + (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules); (*--------------------------------------------------------------------------- * Three postprocessors are applied to the definition. It @@ -79,7 +79,7 @@ val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) - val cntxt = union (op aconv) (cntxtl, cntxtr) + val cntxt = union (op aconv) cntxtl cntxtr in R.GEN_ALL (R.DISCH_ALL diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 12:02:56 2009 +0200 @@ -531,7 +531,7 @@ then writeln (cat_lines ("Extractants =" :: map (Display.string_of_thm_global thy) extractants)) else () - val TCs = List.foldr (union (op aconv)) [] TCl + val TCs = List.foldr (uncurry (union (op aconv))) [] TCl val full_rqt = WFR::TCs val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} val R'abs = S.rand R' diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:02:56 2009 +0200 @@ -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, _, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case x of Prem (us, _, _) => 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,7 +230,7 @@ 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 (union (op =) (arg_vs, in_vs)) ps of + (case check_mode_prems (union (op =) arg_vs in_vs) ps of NONE => false | SOME vs => subset (op =) (concl_vs, vs)) end; diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Wed Oct 21 12:02:56 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 = union (op =) (tfree_lits, tfrees)} + tfrees = union (op =) tfree_lits tfrees} end; val lmap0 = List.foldl (add_thm true) {axioms = [], tfrees = init_tfrees ctxt} cls diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/prop_logic.ML Wed Oct 21 12:02:56 2009 +0200 @@ -111,8 +111,8 @@ | indices False = [] | indices (BoolVar i) = [i] | indices (Not fm) = indices fm - | indices (Or (fm1, fm2)) = union (op =) (indices fm1, indices fm2) - | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2); + | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) + | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); (* ------------------------------------------------------------------------- *) (* maxidx: computes the maximal variable index occuring in a formula of *) diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/refute.ML Wed Oct 21 12:02:56 2009 +0200 @@ -1154,7 +1154,7 @@ val axioms = collect_axioms thy u (* Term.typ list *) val types = Library.foldl (fn (acc, t') => - union (op =) (acc, (ground_types thy t'))) ([], u :: axioms) + uncurry (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))) diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Wed Oct 21 12:02:56 2009 +0200 @@ -473,7 +473,7 @@ val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) (map Thm.term_of hyps) val fixed = OldTerm.term_frees (concl_of st) @ - List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps) + List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps) in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Oct 21 12:02:56 2009 +0200 @@ -93,7 +93,7 @@ val tconst_prefix = "tc_"; val class_prefix = "class_"; -fun union_all xss = List.foldl (union (op =)) [] xss; +fun union_all xss = List.foldl (uncurry (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 (union (op =)) [] (map sorts_on_typs Ts); +fun add_typs Ts = List.foldl (uncurry (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 (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end; + in (union (op =) classes' classes, 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 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 12:02:56 2009 +0200 @@ -155,7 +155,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'), union (op =) (tsP, tsQ)) end + in (CombApp(P',Q'), 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) @@ -167,7 +167,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, union (op =) (ts, ts')) + (Literal(pol,pred)::lits, union (op =) ts ts') end; fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; @@ -476,7 +476,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 (union (op =)) [] tfree_litss) + val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) val _ = File.write_list file ( map (#1 o (clause2tptp params)) axclauses @ diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 12:02:56 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 (union (op =)) [] (map (replace_dep (old, new)) deps)); + (lno, t, List.foldl (uncurry (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 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/sat_solver.ML Wed Oct 21 12:02:56 2009 +0200 @@ -472,7 +472,7 @@ | forced_vars (BoolVar i) = [i] | forced_vars (Not (BoolVar i)) = [~i] | forced_vars (Or (fm1, fm2)) = inter (op =) (forced_vars fm1, forced_vars fm2) - | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1, forced_vars fm2) + | forced_vars (And (fm1, fm2)) = 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 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Tools/transfer.ML Wed Oct 21 12:02:56 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 - (union (op =) (hints1, hints2))} + (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 = union (op =) (hints1, hints2)} + {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = union (op =) hints1 hints2} end; fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) = diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/ex/Codegenerator_Candidates.thy --- a/src/HOL/ex/Codegenerator_Candidates.thy Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Wed Oct 21 12:02:56 2009 +0200 @@ -26,7 +26,7 @@ "~~/src/HOL/ex/Records" begin -(*avoid popular infixes*) -code_reserved SML union inter upto +(*avoid popular infix*) +code_reserved SML upto end diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Wed Oct 21 12:02:56 2009 +0200 @@ -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, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => 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' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of + (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) - (union (op =) (vs, generator_vs)) ps + (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, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => 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,7 +987,7 @@ 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 [] (union (op =) (param_vs, in_vs)) ps of + case check_mode_prems [] (union (op =) param_vs in_vs) ps of NONE => NONE | SOME (acc_ps, vs) => if with_generator then diff -r 6793b02a3409 -r ddf1f03a9ad9 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Oct 21 12:02:56 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 => union (op =) (l, cs)) eqs [] + fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |> filter (fn i => i <> 0) |> sort (int_ord o pairself abs) |> hd @@ -429,9 +429,8 @@ val warning_count = Unsynchronized.ref 0; val warning_count_max = 10; -val union_term = curry (union Pattern.aeconv); -val union_bterm = curry (union - (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'))); +val union_term = union Pattern.aeconv; +val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')); fun add_atoms (lhs, _, _, rhs, _, _) = union_term (map fst lhs) o union_term (map fst rhs); diff -r 6793b02a3409 -r ddf1f03a9ad9 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Wed Oct 21 12:02:56 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, union (op =) + val cs' = map (fn p => (true, p, uncurry (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 6793b02a3409 -r ddf1f03a9ad9 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Oct 21 12:02:56 2009 +0200 @@ -101,7 +101,7 @@ val tos = connected_with chains' [lhs] [lhs]; in (copy_lookahead tos [], - union (op =) (if member (op =) lambdas lhs then tos else [], lambdas)) + union (op =) (if member (op =) lambdas lhs then tos else []) lambdas) end; (*test if new production can produce lambda @@ -109,7 +109,7 @@ val (new_lambda, lambdas') = if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id | (Terminal _) => false) rhs then - (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs])) + (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs])) else (false, lambdas'); @@ -125,7 +125,7 @@ (*get all known starting tokens for a nonterminal*) fun starts_for_nt nt = snd (fst (Array.sub (prods, nt))); - val token_union = union matching_tokens; + val token_union = uncurry (union matching_tokens); (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = @@ -155,7 +155,7 @@ val added_tks' = token_union (new_tks, added_tks); - val nt_dependencies' = union (op =) (nts, nt_dependencies); + val nt_dependencies' = union (op =) nts nt_dependencies; (*associate production with new starting tokens*) fun copy ([]: token option list) nt_prods = nt_prods @@ -413,7 +413,7 @@ fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); val nt_prods = - Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @ + Library.foldl (uncurry (union (op =))) ([], map snd (snd (Array.sub (prods, tag)))) @ map prod_of_chain ((these o AList.lookup (op =) chains) tag); in map (pretty_prod name) nt_prods end; @@ -562,8 +562,8 @@ fun process_nt ~1 result = result | process_nt nt result = let - val nt_prods = Library.foldl (union op =) - ([], map snd (snd (Array.sub (prods2, nt)))); + val nt_prods = Library.foldl (uncurry (union (op =))) + ([], map snd (snd (Array.sub (prods2, nt)))); val lhs_tag = convert_tag nt; (*convert tags in rhs*) diff -r 6793b02a3409 -r ddf1f03a9ad9 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Wed Oct 21 12:02:56 2009 +0200 @@ -352,7 +352,7 @@ in SynExt { xprods = xprods, - consts = union (op =) (consts, mfix_consts), + consts = 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 6793b02a3409 -r ddf1f03a9ad9 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Pure/codegen.ML Wed Oct 21 12:02:56 2009 +0200 @@ -599,8 +599,8 @@ else Pretty.block (separate (Pretty.brk 1) (p :: ps)); fun new_names t xs = Name.variant_list - (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); + (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 6793b02a3409 -r ddf1f03a9ad9 src/Pure/library.ML --- a/src/Pure/library.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Pure/library.ML Wed Oct 21 12:02:56 2009 +0200 @@ -157,12 +157,12 @@ val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list + val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list val subtract: ('b * 'a -> 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 union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool @@ -784,6 +784,7 @@ fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs; fun update eq x xs = cons x (remove eq x xs); +fun union eq = fold (insert eq); fun subtract eq = fold (remove eq); fun merge eq (xs, ys) = @@ -798,11 +799,6 @@ fun (x: int) mem_int xs = member (op =) xs x; fun (x: string) mem_string xs = member (op =) xs x; -(*union of sets represented as lists: no repetitions*) -fun union eq (xs, []) = xs - | union eq ([], ys) = ys - | union eq (x :: xs, ys) = union eq (xs, insert eq x ys); - (*intersection*) fun inter eq ([], ys) = [] | inter eq (x::xs, ys) = diff -r 6793b02a3409 -r ddf1f03a9ad9 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Pure/proofterm.ML Wed Oct 21 12:02:56 2009 +0200 @@ -900,7 +900,7 @@ fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then - union (op =) (vs, map_filter (fn Var (ixn, T) => + union (op =) vs (map_filter (fn Var (ixn, T) => if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs; @@ -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) = union (op =) (prop_vars P, prop_vars Q) +fun prop_vars (Const ("==>", _) $ P $ Q) = 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 = - union (op =) (Library.foldl (union (op =)) - ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))), - prop_vars prop); + union (op =) (Library.foldl (uncurry (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 (union (op =) (is, is'), ch orelse ch', ts', + in (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 union (op =) (ixns, ixns') else ixns' - | _ => union (op =) (ixns, ixns'))) + SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns' + | _ => 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) = - union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs) + 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 6793b02a3409 -r ddf1f03a9ad9 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Oct 21 12:02:56 2009 +0200 @@ -139,13 +139,11 @@ val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds); val (conds_tyvs,cond_vs) = Library.foldl (fn ((tyvs, vs), t) => - (union (op =) - (OldTerm.term_tvars t, tyvs), - union (op =) - (map Term.dest_Var (OldTerm.term_vars t), vs))) + (union (op =) (OldTerm.term_tvars t) tyvs, + 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 = union (op =) (termvars, cond_vs); + val vars_to_fix = union (op =) termvars cond_vs; val (renamings, names2) = List.foldr (fn (((n,i),ty), (vs, names')) => let val n' = Name.variant names' n in