curried union as canonical list operation
authorhaftmann
Wed Oct 21 12:02:56 2009 +0200 (2009-10-21)
changeset 33042ddf1f03a9ad9
parent 33041 6793b02a3409
child 33043 ff71cadefb14
curried union as canonical list operation
src/HOL/Import/hol4rews.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/SEQ.thy
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_solver.ML
src/HOL/Tools/transfer.ML
src/HOL/ex/Codegenerator_Candidates.thy
src/HOL/ex/predicate_compile.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/codegen.ML
src/Pure/library.ML
src/Pure/proofterm.ML
src/Tools/IsaPlanner/rw_inst.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Wed Oct 21 12:02:19 2009 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Wed Oct 21 12:02:56 2009 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4    val empty = []
     1.5    val copy = I
     1.6    val extend = I
     1.7 -  fun merge _ = Library.union Thm.eq_thm
     1.8 +  fun merge _ = Library.merge Thm.eq_thm_prop
     1.9  )
    1.10  
    1.11  val hol4_debug = Unsynchronized.ref false
     2.1 --- a/src/HOL/Import/shuffler.ML	Wed Oct 21 12:02:19 2009 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Wed Oct 21 12:02:56 2009 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4    val empty = []
     2.5    val copy = I
     2.6    val extend = I
     2.7 -  fun merge _ = Library.union Thm.eq_thm
     2.8 +  fun merge _ = Library.merge Thm.eq_thm_prop
     2.9  )
    2.10  
    2.11  fun print_shuffles thy =
     3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 12:02:19 2009 +0200
     3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 12:02:56 2009 +0200
     3.3 @@ -244,7 +244,7 @@
     3.4  
     3.5  fun monomial_lcm m1 m2 =
     3.6    fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
     3.7 -          (union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
     3.8 +          (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1) (FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
     3.9  
    3.10  fun monomial_multidegree m =
    3.11   FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
    3.12 @@ -314,7 +314,7 @@
    3.13    FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
    3.14  
    3.15  fun poly_variables p =
    3.16 -  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
    3.17 +  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);;
    3.18  
    3.19  (* Order monomials for human presentation.                                   *)
    3.20  
    3.21 @@ -1059,8 +1059,8 @@
    3.22  
    3.23  fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
    3.24  let
    3.25 - val vars = fold_rev (curry (union (op aconvc)) o poly_variables)
    3.26 -              (pol::eqs @ map fst leqs) []
    3.27 + val vars = fold_rev (union (op aconvc) o poly_variables)
    3.28 +   (pol :: eqs @ map fst leqs) []
    3.29   val monoid = if linf then
    3.30        (poly_const rat_1,RealArith.Rational_lt rat_1)::
    3.31        (filter (fn (p,c) => multidegree p <= d) leqs)
     4.1 --- a/src/HOL/Library/normarith.ML	Wed Oct 21 12:02:19 2009 +0200
     4.2 +++ b/src/HOL/Library/normarith.ML	Wed Oct 21 12:02:56 2009 +0200
     4.3 @@ -286,7 +286,7 @@
     4.4     val dests = distinct (op aconvc) (map snd rawdests)
     4.5     val srcfuns = map vector_lincomb sources
     4.6     val destfuns = map vector_lincomb dests 
     4.7 -   val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
     4.8 +   val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
     4.9     val n = length srcfuns
    4.10     val nvs = 1 upto n
    4.11     val srccombs = srcfuns ~~ nvs
     5.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 12:02:19 2009 +0200
     5.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 12:02:56 2009 +0200
     5.3 @@ -620,7 +620,7 @@
     5.4    | NONE => (case eqs of 
     5.5      [] => 
     5.6       let val vars = remove (op aconvc) one_tm 
     5.7 -           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
     5.8 +           (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
     5.9       in linear_ineqs vars (les,lts) end
    5.10     | (e,p)::es => 
    5.11       if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
    5.12 @@ -679,7 +679,7 @@
    5.13    val le_pols = map rhs le
    5.14    val lt_pols = map rhs lt 
    5.15    val aliens =  filter is_alien
    5.16 -      (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
    5.17 +      (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) 
    5.18            (eq_pols @ le_pols @ lt_pols) [])
    5.19    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
    5.20    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
     6.1 --- a/src/HOL/SEQ.thy	Wed Oct 21 12:02:19 2009 +0200
     6.2 +++ b/src/HOL/SEQ.thy	Wed Oct 21 12:02:56 2009 +0200
     6.3 @@ -1089,10 +1089,10 @@
     6.4  
     6.5  subsubsection {* Cauchy Sequences are Convergent *}
     6.6  
     6.7 -axclass complete_space \<subseteq> metric_space
     6.8 -  Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
     6.9 +class complete_space =
    6.10 +  assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
    6.11  
    6.12 -axclass banach \<subseteq> real_normed_vector, complete_space
    6.13 +class banach = real_normed_vector + complete_space
    6.14  
    6.15  theorem LIMSEQ_imp_Cauchy:
    6.16    assumes X: "X ----> a" shows "Cauchy X"
     7.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Oct 21 12:02:19 2009 +0200
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Oct 21 12:02:56 2009 +0200
     7.3 @@ -257,7 +257,7 @@
     7.4  fun get_nonrec_types descr sorts =
     7.5    map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
     7.6      Library.foldl (fn (Ts', (_, cargs)) =>
     7.7 -      union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
     7.8 +      union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr));
     7.9  
    7.10  (* get all recursive types in datatype description *)
    7.11  
     8.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:02:19 2009 +0200
     8.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:02:56 2009 +0200
     8.3 @@ -348,7 +348,7 @@
     8.4    | Add(lin1,lin2) =>
     8.5          let val lis1 = resolve_proof vars lin1
     8.6              val lis2 = resolve_proof vars lin2
     8.7 -            val dom = distinct (op =) (union (op =) (map fst lis1, map fst lis2))
     8.8 +            val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2))
     8.9          in
    8.10              map (fn n => let val a = these (AList.lookup (op =) lis1 n)
    8.11                               val b = these (AList.lookup (op =) lis2 n)
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 12:02:19 2009 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 12:02:56 2009 +0200
     9.3 @@ -1047,16 +1047,16 @@
     9.4              (if with_generator then
     9.5                (case select_mode_prem thy gen_modes' vs ps of
     9.6                  SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
     9.7 -                  (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
     9.8 +                  (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
     9.9                    (filter_out (equal p) ps)
    9.10                | _ =>
    9.11                    let 
    9.12                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
    9.13                    in
    9.14                      case (find_first (fn generator_vs => is_some
    9.15 -                      (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
    9.16 +                      (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of
    9.17                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
    9.18 -                        (union (op =) (vs, generator_vs)) ps
    9.19 +                        (union (op =) vs generator_vs) ps
    9.20                      | NONE => let
    9.21                      val _ = tracing ("ps:" ^ (commas
    9.22                      (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
    9.23 @@ -1065,7 +1065,7 @@
    9.24              else
    9.25                NONE)
    9.26          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
    9.27 -            (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
    9.28 +            (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
    9.29              (filter_out (equal p) ps))
    9.30      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
    9.31      val in_vs = terms_vs in_ts;
    9.32 @@ -1073,7 +1073,7 @@
    9.33    in
    9.34      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
    9.35      forall (is_eqT o fastype_of) in_ts' then
    9.36 -      case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
    9.37 +      case check_mode_prems [] (union (op =) param_vs in_vs) ps of
    9.38           NONE => NONE
    9.39         | SOME (acc_ps, vs) =>
    9.40           if with_generator then
    10.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 12:02:19 2009 +0200
    10.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 12:02:56 2009 +0200
    10.3 @@ -308,7 +308,7 @@
    10.4    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
    10.5    | _ => (acc, dacc)
    10.6    val (cs,ds) = h ([],[]) p
    10.7 -  val l = Integer.lcms (union (op =) (cs, ds))
    10.8 +  val l = Integer.lcms (union (op =) cs ds)
    10.9    fun cv k ct =
   10.10      let val (tm as b$s$t) = term_of ct
   10.11      in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
    11.1 --- a/src/HOL/Tools/TFL/post.ML	Wed Oct 21 12:02:19 2009 +0200
    11.2 +++ b/src/HOL/Tools/TFL/post.ML	Wed Oct 21 12:02:56 2009 +0200
    11.3 @@ -28,7 +28,7 @@
    11.4   *--------------------------------------------------------------------------*)
    11.5  fun termination_goals rules =
    11.6      map (Type.freeze o HOLogic.dest_Trueprop)
    11.7 -      (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules);
    11.8 +      (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules);
    11.9  
   11.10  (*---------------------------------------------------------------------------
   11.11   * Three postprocessors are applied to the definition.  It
   11.12 @@ -79,7 +79,7 @@
   11.13        val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   11.14        val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   11.15        val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   11.16 -      val cntxt = union (op aconv) (cntxtl, cntxtr)
   11.17 +      val cntxt = union (op aconv) cntxtl cntxtr
   11.18    in
   11.19      R.GEN_ALL
   11.20        (R.DISCH_ALL
    12.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 12:02:19 2009 +0200
    12.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 12:02:56 2009 +0200
    12.3 @@ -531,7 +531,7 @@
    12.4                   then writeln (cat_lines ("Extractants =" ::
    12.5                    map (Display.string_of_thm_global thy) extractants))
    12.6                   else ()
    12.7 -     val TCs = List.foldr (union (op aconv)) [] TCl
    12.8 +     val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
    12.9       val full_rqt = WFR::TCs
   12.10       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   12.11       val R'abs = S.rand R'
    13.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 12:02:19 2009 +0200
    13.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 12:02:56 2009 +0200
    13.3 @@ -222,7 +222,7 @@
    13.4        | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
    13.5            NONE => NONE
    13.6          | SOME (x, _) => check_mode_prems
    13.7 -            (case x of Prem (us, _, _) => union (op =) (vs, terms_vs us) | _ => vs)
    13.8 +            (case x of Prem (us, _, _) => union (op =) vs (terms_vs us) | _ => vs)
    13.9              (filter_out (equal x) ps));
   13.10      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
   13.11      val in_vs = terms_vs in_ts;
   13.12 @@ -230,7 +230,7 @@
   13.13    in
   13.14      forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   13.15      forall (is_eqT o fastype_of) in_ts' andalso
   13.16 -    (case check_mode_prems (union (op =) (arg_vs, in_vs)) ps of
   13.17 +    (case check_mode_prems (union (op =) arg_vs in_vs) ps of
   13.18         NONE => false
   13.19       | SOME vs => subset (op =) (concl_vs, vs))
   13.20    end;
    14.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Oct 21 12:02:19 2009 +0200
    14.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 21 12:02:56 2009 +0200
    14.3 @@ -631,7 +631,7 @@
    14.4          let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
    14.5          in
    14.6             {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
    14.7 -            tfrees = union (op =) (tfree_lits, tfrees)}
    14.8 +            tfrees = union (op =) tfree_lits tfrees}
    14.9          end;
   14.10        val lmap0 = List.foldl (add_thm true)
   14.11                          {axioms = [], tfrees = init_tfrees ctxt} cls
    15.1 --- a/src/HOL/Tools/prop_logic.ML	Wed Oct 21 12:02:19 2009 +0200
    15.2 +++ b/src/HOL/Tools/prop_logic.ML	Wed Oct 21 12:02:56 2009 +0200
    15.3 @@ -111,8 +111,8 @@
    15.4  	  | indices False            = []
    15.5  	  | indices (BoolVar i)      = [i]
    15.6  	  | indices (Not fm)         = indices fm
    15.7 -	  | indices (Or (fm1, fm2))  = union (op =) (indices fm1, indices fm2)
    15.8 -	  | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2);
    15.9 +	  | indices (Or (fm1, fm2))  = union (op =) (indices fm1) (indices fm2)
   15.10 +	  | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
   15.11  
   15.12  (* ------------------------------------------------------------------------- *)
   15.13  (* maxidx: computes the maximal variable index occuring in a formula of      *)
    16.1 --- a/src/HOL/Tools/refute.ML	Wed Oct 21 12:02:19 2009 +0200
    16.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 21 12:02:56 2009 +0200
    16.3 @@ -1154,7 +1154,7 @@
    16.4        val axioms = collect_axioms thy u
    16.5        (* Term.typ list *)
    16.6        val types = Library.foldl (fn (acc, t') =>
    16.7 -        union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
    16.8 +        uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms)
    16.9        val _     = tracing ("Ground types: "
   16.10          ^ (if null types then "none."
   16.11             else commas (map (Syntax.string_of_typ_global thy) types)))
    17.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Oct 21 12:02:19 2009 +0200
    17.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Oct 21 12:02:56 2009 +0200
    17.3 @@ -473,7 +473,7 @@
    17.4        val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
    17.5                                        (map Thm.term_of hyps)
    17.6        val fixed = OldTerm.term_frees (concl_of st) @
    17.7 -                  List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
    17.8 +                  List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps)
    17.9    in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   17.10  
   17.11  
    18.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 21 12:02:19 2009 +0200
    18.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 21 12:02:56 2009 +0200
    18.3 @@ -93,7 +93,7 @@
    18.4  val tconst_prefix = "tc_";
    18.5  val class_prefix = "class_";
    18.6  
    18.7 -fun union_all xss = List.foldl (union (op =)) [] xss;
    18.8 +fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
    18.9  
   18.10  (*Provide readable names for the more common symbolic functions*)
   18.11  val const_trans_table =
   18.12 @@ -263,7 +263,7 @@
   18.13    | pred_of_sort (LTFree (s,ty)) = (s,1)
   18.14  
   18.15  (*Given a list of sorted type variables, return a list of type literals.*)
   18.16 -fun add_typs Ts = List.foldl (union (op =)) [] (map sorts_on_typs Ts);
   18.17 +fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts);
   18.18  
   18.19  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   18.20    * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   18.21 @@ -372,7 +372,7 @@
   18.22        let val cpairs = type_class_pairs thy tycons classes
   18.23            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
   18.24            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   18.25 -      in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;
   18.26 +      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   18.27  
   18.28  fun make_arity_clauses_dfg dfg thy tycons classes =
   18.29    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
    19.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 12:02:19 2009 +0200
    19.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 12:02:56 2009 +0200
    19.3 @@ -155,7 +155,7 @@
    19.4    | combterm_of dfg thy (P $ Q) =
    19.5        let val (P',tsP) = combterm_of dfg thy P
    19.6            val (Q',tsQ) = combterm_of dfg thy Q
    19.7 -      in  (CombApp(P',Q'), union (op =) (tsP, tsQ))  end
    19.8 +      in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
    19.9    | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
   19.10  
   19.11  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
   19.12 @@ -167,7 +167,7 @@
   19.13    | literals_of_term1 dfg thy (lits,ts) P =
   19.14        let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   19.15        in
   19.16 -          (Literal(pol,pred)::lits, union (op =) (ts, ts'))
   19.17 +          (Literal(pol,pred)::lits, union (op =) ts ts')
   19.18        end;
   19.19  
   19.20  fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   19.21 @@ -476,7 +476,7 @@
   19.22      val (cma, cnh) = count_constants clauses
   19.23      val params = (t_full, cma, cnh)
   19.24      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   19.25 -    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (union (op =)) [] tfree_litss)
   19.26 +    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   19.27      val _ =
   19.28        File.write_list file (
   19.29          map (#1 o (clause2tptp params)) axclauses @
    20.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 12:02:19 2009 +0200
    20.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 12:02:56 2009 +0200
    20.3 @@ -364,7 +364,7 @@
    20.4  fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
    20.5  
    20.6  fun replace_deps (old:int, new) (lno, t, deps) =
    20.7 -      (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps));
    20.8 +      (lno, t, List.foldl (uncurry (union (op =))) [] (map (replace_dep (old, new)) deps));
    20.9  
   20.10  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   20.11    only in type information.*)
    21.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:02:19 2009 +0200
    21.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:02:56 2009 +0200
    21.3 @@ -472,7 +472,7 @@
    21.4          | forced_vars (BoolVar i)       = [i]
    21.5          | forced_vars (Not (BoolVar i)) = [~i]
    21.6          | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1, forced_vars fm2)
    21.7 -        | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1, forced_vars fm2)
    21.8 +        | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1) (forced_vars fm2)
    21.9          (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   21.10          (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   21.11          | forced_vars _                 = error "formula is not in negation normal form"
    22.1 --- a/src/HOL/Tools/transfer.ML	Wed Oct 21 12:02:19 2009 +0200
    22.2 +++ b/src/HOL/Tools/transfer.ML	Wed Oct 21 12:02:56 2009 +0200
    22.3 @@ -143,7 +143,7 @@
    22.4   {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
    22.5    ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
    22.6    hints = subtract (op = : string*string -> bool) hints0
    22.7 -            (union (op =) (hints1, hints2))}
    22.8 +            (union (op =) hints1 hints2)}
    22.9   end;
   22.10  
   22.11  local
   22.12 @@ -151,7 +151,7 @@
   22.13  in
   22.14  fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
   22.15                     {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
   22.16 -    {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)}
   22.17 +    {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}
   22.18  end;
   22.19  
   22.20  fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
    23.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Wed Oct 21 12:02:19 2009 +0200
    23.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Wed Oct 21 12:02:56 2009 +0200
    23.3 @@ -26,7 +26,7 @@
    23.4    "~~/src/HOL/ex/Records"
    23.5  begin
    23.6  
    23.7 -(*avoid popular infixes*)
    23.8 -code_reserved SML union inter upto
    23.9 +(*avoid popular infix*)
   23.10 +code_reserved SML upto
   23.11  
   23.12  end
    24.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Oct 21 12:02:19 2009 +0200
    24.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Oct 21 12:02:56 2009 +0200
    24.3 @@ -964,22 +964,22 @@
    24.4              (if with_generator then
    24.5                (case select_mode_prem thy gen_modes' vs ps of
    24.6                    SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
    24.7 -                  (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
    24.8 +                  (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
    24.9                    (filter_out (equal p) ps)
   24.10                  | NONE =>
   24.11                    let 
   24.12                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
   24.13                    in
   24.14                      case (find_first (fn generator_vs => is_some
   24.15 -                      (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
   24.16 +                      (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of
   24.17                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
   24.18 -                        (union (op =) (vs, generator_vs)) ps
   24.19 +                        (union (op =) vs generator_vs) ps
   24.20                      | NONE => NONE
   24.21                    end)
   24.22              else
   24.23                NONE)
   24.24          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
   24.25 -            (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
   24.26 +            (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
   24.27              (filter_out (equal p) ps))
   24.28      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
   24.29      val in_vs = terms_vs in_ts;
   24.30 @@ -987,7 +987,7 @@
   24.31    in
   24.32      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   24.33      forall (is_eqT o fastype_of) in_ts' then
   24.34 -      case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
   24.35 +      case check_mode_prems [] (union (op =) param_vs in_vs) ps of
   24.36           NONE => NONE
   24.37         | SOME (acc_ps, vs) =>
   24.38           if with_generator then
    25.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Oct 21 12:02:19 2009 +0200
    25.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Oct 21 12:02:56 2009 +0200
    25.3 @@ -385,7 +385,7 @@
    25.4    let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
    25.5    if not (null eqs) then
    25.6       let val c =
    25.7 -           fold (fn Lineq(_,_,l,_) => fn cs => union (op =) (l, cs)) eqs []
    25.8 +           fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs []
    25.9             |> filter (fn i => i <> 0)
   25.10             |> sort (int_ord o pairself abs)
   25.11             |> hd
   25.12 @@ -429,9 +429,8 @@
   25.13  val warning_count = Unsynchronized.ref 0;
   25.14  val warning_count_max = 10;
   25.15  
   25.16 -val union_term = curry (union Pattern.aeconv);
   25.17 -val union_bterm = curry (union
   25.18 -  (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
   25.19 +val union_term = union Pattern.aeconv;
   25.20 +val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
   25.21  
   25.22  fun add_atoms (lhs, _, _, rhs, _, _) =
   25.23    union_term (map fst lhs) o union_term (map fst rhs);
    26.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Oct 21 12:02:19 2009 +0200
    26.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Oct 21 12:02:56 2009 +0200
    26.3 @@ -289,7 +289,7 @@
    26.4      val _ = message "Collecting constraints...";
    26.5      val (t, prf, cs, env, _) = make_constraints_cprf thy
    26.6        (Envir.empty (maxidx_proof cprf ~1)) cprf';
    26.7 -    val cs' = map (fn p => (true, p, union (op =) 
    26.8 +    val cs' = map (fn p => (true, p, uncurry (union (op =)) 
    26.9          (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
   26.10        (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
   26.11      val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
    27.1 --- a/src/Pure/Syntax/parser.ML	Wed Oct 21 12:02:19 2009 +0200
    27.2 +++ b/src/Pure/Syntax/parser.ML	Wed Oct 21 12:02:56 2009 +0200
    27.3 @@ -101,7 +101,7 @@
    27.4  
    27.5              val tos = connected_with chains' [lhs] [lhs];
    27.6          in (copy_lookahead tos [],
    27.7 -            union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
    27.8 +            union (op =) (if member (op =) lambdas lhs then tos else []) lambdas)
    27.9          end;
   27.10  
   27.11        (*test if new production can produce lambda
   27.12 @@ -109,7 +109,7 @@
   27.13        val (new_lambda, lambdas') =
   27.14          if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
   27.15                      | (Terminal _) => false) rhs then
   27.16 -          (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
   27.17 +          (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs]))
   27.18          else
   27.19            (false, lambdas');
   27.20  
   27.21 @@ -125,7 +125,7 @@
   27.22        (*get all known starting tokens for a nonterminal*)
   27.23        fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
   27.24  
   27.25 -      val token_union = union matching_tokens;
   27.26 +      val token_union = uncurry (union matching_tokens);
   27.27  
   27.28        (*update prods, lookaheads, and lambdas according to new lambda NTs*)
   27.29        val (added_starts', lambdas') =
   27.30 @@ -155,7 +155,7 @@
   27.31  
   27.32                          val added_tks' = token_union (new_tks, added_tks);
   27.33  
   27.34 -                        val nt_dependencies' = union (op =) (nts, nt_dependencies);
   27.35 +                        val nt_dependencies' = union (op =) nts nt_dependencies;
   27.36  
   27.37                          (*associate production with new starting tokens*)
   27.38                          fun copy ([]: token option list) nt_prods = nt_prods
   27.39 @@ -413,7 +413,7 @@
   27.40          fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
   27.41  
   27.42          val nt_prods =
   27.43 -          Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
   27.44 +          Library.foldl (uncurry (union (op =))) ([], map snd (snd (Array.sub (prods, tag)))) @
   27.45            map prod_of_chain ((these o AList.lookup (op =) chains) tag);
   27.46        in map (pretty_prod name) nt_prods end;
   27.47  
   27.48 @@ -562,8 +562,8 @@
   27.49      fun process_nt ~1 result = result
   27.50        | process_nt nt result =
   27.51          let
   27.52 -          val nt_prods = Library.foldl (union op =)
   27.53 -                             ([], map snd (snd (Array.sub (prods2, nt))));
   27.54 +          val nt_prods = Library.foldl (uncurry (union (op =)))
   27.55 +            ([], map snd (snd (Array.sub (prods2, nt))));
   27.56            val lhs_tag = convert_tag nt;
   27.57  
   27.58            (*convert tags in rhs*)
    28.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Oct 21 12:02:19 2009 +0200
    28.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Oct 21 12:02:56 2009 +0200
    28.3 @@ -352,7 +352,7 @@
    28.4    in
    28.5      SynExt {
    28.6        xprods = xprods,
    28.7 -      consts = union (op =) (consts, mfix_consts),
    28.8 +      consts = union (op =) consts mfix_consts,
    28.9        prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
   28.10        parse_ast_translation = parse_ast_translation,
   28.11        parse_rules = parse_rules' @ parse_rules,
    29.1 --- a/src/Pure/codegen.ML	Wed Oct 21 12:02:19 2009 +0200
    29.2 +++ b/src/Pure/codegen.ML	Wed Oct 21 12:02:56 2009 +0200
    29.3 @@ -599,8 +599,8 @@
    29.4       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
    29.5  
    29.6  fun new_names t xs = Name.variant_list
    29.7 -  (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
    29.8 -    OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
    29.9 +  (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t))
   29.10 +    (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
   29.11  
   29.12  fun new_name t x = hd (new_names t [x]);
   29.13  
    30.1 --- a/src/Pure/library.ML	Wed Oct 21 12:02:19 2009 +0200
    30.2 +++ b/src/Pure/library.ML	Wed Oct 21 12:02:56 2009 +0200
    30.3 @@ -157,12 +157,12 @@
    30.4    val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    30.5    val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    30.6    val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    30.7 +  val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    30.8    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
    30.9    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   30.10    val mem: ''a * ''a list -> bool
   30.11    val mem_int: int * int list -> bool
   30.12    val mem_string: string * string list -> bool
   30.13 -  val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   30.14    val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   30.15    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   30.16    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   30.17 @@ -784,6 +784,7 @@
   30.18  fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
   30.19  fun update eq x xs = cons x (remove eq x xs);
   30.20  
   30.21 +fun union eq = fold (insert eq);
   30.22  fun subtract eq = fold (remove eq);
   30.23  
   30.24  fun merge eq (xs, ys) =
   30.25 @@ -798,11 +799,6 @@
   30.26  fun (x: int) mem_int xs = member (op =) xs x;
   30.27  fun (x: string) mem_string xs = member (op =) xs x;
   30.28  
   30.29 -(*union of sets represented as lists: no repetitions*)
   30.30 -fun union eq (xs, []) = xs
   30.31 -  | union eq ([], ys) = ys
   30.32 -  | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
   30.33 -
   30.34  (*intersection*)
   30.35  fun inter eq ([], ys) = []
   30.36    | inter eq (x::xs, ys) =
    31.1 --- a/src/Pure/proofterm.ML	Wed Oct 21 12:02:19 2009 +0200
    31.2 +++ b/src/Pure/proofterm.ML	Wed Oct 21 12:02:56 2009 +0200
    31.3 @@ -900,7 +900,7 @@
    31.4  
    31.5  fun add_funvars Ts (vs, t) =
    31.6    if is_fun (fastype_of1 (Ts, t)) then
    31.7 -    union (op =) (vs, map_filter (fn Var (ixn, T) =>
    31.8 +    union (op =) vs (map_filter (fn Var (ixn, T) =>
    31.9        if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
   31.10    else vs;
   31.11  
   31.12 @@ -918,7 +918,7 @@
   31.13    | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   31.14    | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
   31.15  
   31.16 -fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P, prop_vars Q)
   31.17 +fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
   31.18    | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
   31.19    | prop_vars t = (case strip_comb t of
   31.20        (Var (ixn, _), _) => [ixn] | _ => []);
   31.21 @@ -936,9 +936,9 @@
   31.22    end;
   31.23  
   31.24  fun needed_vars prop =
   31.25 -  union (op =) (Library.foldl (union (op =))
   31.26 -    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
   31.27 -  prop_vars prop);
   31.28 +  union (op =) (Library.foldl (uncurry (union (op =)))
   31.29 +    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))))
   31.30 +  (prop_vars prop);
   31.31  
   31.32  fun gen_axm_proof c name prop =
   31.33    let
   31.34 @@ -975,7 +975,7 @@
   31.35            let
   31.36              val p as (_, is', ch', prf') = shrink ls lev prf2;
   31.37              val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
   31.38 -          in (union (op =) (is, is'), ch orelse ch', ts',
   31.39 +          in (union (op =) is is', ch orelse ch', ts',
   31.40                if ch orelse ch' then prf'' %% prf' else prf)
   31.41            end
   31.42        | shrink' ls lev ts prfs (prf as prf1 % t) =
   31.43 @@ -1004,15 +1004,15 @@
   31.44              val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
   31.45              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
   31.46                insert (op =) ixn (case AList.lookup (op =) insts ixn of
   31.47 -                  SOME (SOME t) => if is_proj t then union (op =) (ixns, ixns') else ixns'
   31.48 -                | _ => union (op =) (ixns, ixns')))
   31.49 +                  SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
   31.50 +                | _ => union (op =) ixns ixns'))
   31.51                    (needed prop ts'' prfs, add_npvars false true [] ([], prop));
   31.52              val insts' = map
   31.53                (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
   31.54                  | (_, x) => (false, x)) insts
   31.55            in ([], false, insts' @ map (pair false) ts'', prf) end
   31.56      and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
   31.57 -          union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
   31.58 +          union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
   31.59        | needed (Var (ixn, _)) (_::_) _ = [ixn]
   31.60        | needed _ _ _ = [];
   31.61    in shrink end;
    32.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Oct 21 12:02:19 2009 +0200
    32.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Oct 21 12:02:56 2009 +0200
    32.3 @@ -139,13 +139,11 @@
    32.4        val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
    32.5        val (conds_tyvs,cond_vs) = 
    32.6            Library.foldl (fn ((tyvs, vs), t) => 
    32.7 -                    (union (op =)
    32.8 -                       (OldTerm.term_tvars t, tyvs),
    32.9 -                     union (op =)
   32.10 -                       (map Term.dest_Var (OldTerm.term_vars t), vs))) 
   32.11 +                    (union (op =) (OldTerm.term_tvars t) tyvs,
   32.12 +                     union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs))
   32.13                  (([],[]), rule_conds);
   32.14        val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
   32.15 -      val vars_to_fix = union (op =) (termvars, cond_vs);
   32.16 +      val vars_to_fix = union (op =) termvars cond_vs;
   32.17        val (renamings, names2) = 
   32.18            List.foldr (fn (((n,i),ty), (vs, names')) => 
   32.19                      let val n' = Name.variant names' n in