merged
authorhaftmann
Wed Oct 21 08:16:25 2009 +0200 (2009-10-21)
changeset 330395018f6a76b3f
parent 33036 c61fe520602b
parent 33038 8f9594c31de4
child 33040 cffdb7b28498
child 33041 6793b02a3409
merged
src/HOL/Import/proof_kernel.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Set.thy
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/tfl.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/predicate_compile.ML
src/Pure/Tools/find_theorems.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/NEWS	Wed Oct 21 16:41:22 2009 +1100
     1.2 +++ b/NEWS	Wed Oct 21 08:16:25 2009 +0200
     1.3 @@ -213,6 +213,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Removed some old-style infix operations using polymorphic equality.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
    1.11  provides a high-level programming interface to synchronized state
    1.12  variables with atomic update.  This works via pure function
     2.1 --- a/src/HOL/Import/hol4rews.ML	Wed Oct 21 16:41:22 2009 +1100
     2.2 +++ b/src/HOL/Import/hol4rews.ML	Wed Oct 21 08:16:25 2009 +0200
     2.3 @@ -165,7 +165,7 @@
     2.4    val empty = []
     2.5    val copy = I
     2.6    val extend = I
     2.7 -  fun merge _ = Library.gen_union Thm.eq_thm
     2.8 +  fun merge _ = Library.union Thm.eq_thm
     2.9  )
    2.10  
    2.11  val hol4_debug = Unsynchronized.ref false
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Oct 21 16:41:22 2009 +1100
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 21 08:16:25 2009 +0200
     3.3 @@ -281,9 +281,10 @@
     3.4            | itr (a::rst) = i=a orelse itr rst
     3.5      in itr L end;
     3.6  
     3.7 +infix union;
     3.8  fun [] union S = S
     3.9    | S union [] = S
    3.10 -  | (a::rst) union S2 = rst union (insert (op =) a S2)
    3.11 +  | (a::rst) union S2 = rst union (insert (op =) a S2);
    3.12  
    3.13  fun implode_subst [] = []
    3.14    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
    3.15 @@ -1229,7 +1230,7 @@
    3.16            | add_consts (_, cs) = cs
    3.17          val t_consts = add_consts(t,[])
    3.18      in
    3.19 -        fn th => eq_set(t_consts,add_consts(prop_of th,[]))
    3.20 +        fn th => eq_set (op =) (t_consts, add_consts (prop_of th, []))
    3.21      end
    3.22  
    3.23  fun split_name str =
     4.1 --- a/src/HOL/Import/shuffler.ML	Wed Oct 21 16:41:22 2009 +1100
     4.2 +++ b/src/HOL/Import/shuffler.ML	Wed Oct 21 08:16:25 2009 +0200
     4.3 @@ -78,7 +78,7 @@
     4.4    val empty = []
     4.5    val copy = I
     4.6    val extend = I
     4.7 -  fun merge _ = Library.gen_union Thm.eq_thm
     4.8 +  fun merge _ = Library.union Thm.eq_thm
     4.9  )
    4.10  
    4.11  fun print_shuffles thy =
    4.12 @@ -563,7 +563,7 @@
    4.13          let
    4.14              val th_consts = add_consts(prop_of th,[])
    4.15          in
    4.16 -            eq_set(t_consts,th_consts)
    4.17 +            eq_set (op =) (t_consts, th_consts)
    4.18          end
    4.19      end
    4.20  
     5.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 16:41:22 2009 +1100
     5.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 08:16:25 2009 +0200
     5.3 @@ -244,7 +244,7 @@
     5.4  
     5.5  fun monomial_lcm m1 m2 =
     5.6    fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
     5.7 -          (gen_union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
     5.8 +          (union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
     5.9  
    5.10  fun monomial_multidegree m =
    5.11   FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
    5.12 @@ -314,7 +314,7 @@
    5.13    FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
    5.14  
    5.15  fun poly_variables p =
    5.16 -  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
    5.17 +  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
    5.18  
    5.19  (* Order monomials for human presentation.                                   *)
    5.20  
    5.21 @@ -1059,7 +1059,7 @@
    5.22  
    5.23  fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
    5.24  let
    5.25 - val vars = fold_rev (curry (gen_union (op aconvc)) o poly_variables)
    5.26 + val vars = fold_rev (curry (union (op aconvc)) o poly_variables)
    5.27                (pol::eqs @ map fst leqs) []
    5.28   val monoid = if linf then
    5.29        (poly_const rat_1,RealArith.Rational_lt rat_1)::
     6.1 --- a/src/HOL/Library/normarith.ML	Wed Oct 21 16:41:22 2009 +1100
     6.2 +++ b/src/HOL/Library/normarith.ML	Wed Oct 21 08:16:25 2009 +0200
     6.3 @@ -286,7 +286,7 @@
     6.4     val dests = distinct (op aconvc) (map snd rawdests)
     6.5     val srcfuns = map vector_lincomb sources
     6.6     val destfuns = map vector_lincomb dests 
     6.7 -   val vvs = fold_rev (curry (gen_union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
     6.8 +   val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
     6.9     val n = length srcfuns
    6.10     val nvs = 1 upto n
    6.11     val srccombs = srcfuns ~~ nvs
     7.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 16:41:22 2009 +1100
     7.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 08:16:25 2009 +0200
     7.3 @@ -568,7 +568,7 @@
     7.4    fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
     7.5    val one_tm = @{cterm "1::real"}
     7.6    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
     7.7 -     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
     7.8 +     ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
     7.9         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
    7.10  
    7.11    fun linear_ineqs vars (les,lts) = 
    7.12 @@ -620,7 +620,7 @@
    7.13    | NONE => (case eqs of 
    7.14      [] => 
    7.15       let val vars = remove (op aconvc) one_tm 
    7.16 -           (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
    7.17 +           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
    7.18       in linear_ineqs vars (les,lts) end
    7.19     | (e,p)::es => 
    7.20       if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
    7.21 @@ -679,7 +679,7 @@
    7.22    val le_pols = map rhs le
    7.23    val lt_pols = map rhs lt 
    7.24    val aliens =  filter is_alien
    7.25 -      (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
    7.26 +      (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
    7.27            (eq_pols @ le_pols @ lt_pols) [])
    7.28    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
    7.29    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
     8.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 16:41:22 2009 +1100
     8.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 08:16:25 2009 +0200
     8.3 @@ -28,7 +28,7 @@
     8.4  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
     8.5    (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
     8.6  
     8.7 -fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
     8.8 +fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
     8.9  
    8.10  val fresh_prod = thm "fresh_prod";
    8.11  
     9.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 16:41:22 2009 +1100
     9.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 08:16:25 2009 +0200
     9.3 @@ -33,7 +33,7 @@
     9.4      [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
     9.5       @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
     9.6  
     9.7 -fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
     9.8 +fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
     9.9  
    9.10  val perm_bool = mk_meta_eq (thm "perm_bool");
    9.11  val perm_boolI = thm "perm_boolI";
    10.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 16:41:22 2009 +1100
    10.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 08:16:25 2009 +0200
    10.3 @@ -228,7 +228,7 @@
    10.4        (case Symtab.lookup dt_info tname of
    10.5            NONE => primrec_err (quote tname ^ " is not a nominal datatype")
    10.6          | SOME dt =>
    10.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
    10.8 +            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
    10.9                (tname, dt)::(find_dts dt_info tnames' tnames)
   10.10              else find_dts dt_info tnames' tnames);
   10.11  
   10.12 @@ -251,7 +251,7 @@
   10.13      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
   10.14        map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
   10.15      val _ =
   10.16 -      (if forall (curry eq_set lsrs) lsrss andalso forall
   10.17 +      (if forall (curry (eq_set (op =)) lsrs) lsrss andalso forall
   10.18           (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
   10.19                 forall (fn (_, (ls', _, rs', _, _)) =>
   10.20                   ls = ls' andalso rs = rs') eqns
   10.21 @@ -276,7 +276,7 @@
   10.22      val defs' = map (make_def lthy fixes fs) defs;
   10.23      val names1 = map snd fnames;
   10.24      val names2 = map fst eqns;
   10.25 -    val _ = if gen_eq_set (op =) (names1, names2) then ()
   10.26 +    val _ = if eq_set (op =) (names1, names2) then ()
   10.27        else primrec_err ("functions " ^ commas_quote names2 ^
   10.28          "\nare not mutually recursive");
   10.29      val (defs_thms, lthy') = lthy |>
    11.1 --- a/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 16:41:22 2009 +1100
    11.2 +++ b/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 08:16:25 2009 +0200
    11.3 @@ -55,7 +55,7 @@
    11.4  fun proper_match ps env =
    11.5    forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
    11.6  
    11.7 -val eq_tab = gen_eq_set (op =) o pairself Vartab.dest
    11.8 +val eq_tab = eq_set (op =) o pairself Vartab.dest
    11.9  
   11.10  fun specialize thy cs is ((r, ps), ces) (ts, ns) =
   11.11    let
    12.1 --- a/src/HOL/Set.thy	Wed Oct 21 16:41:22 2009 +1100
    12.2 +++ b/src/HOL/Set.thy	Wed Oct 21 08:16:25 2009 +0200
    12.3 @@ -303,7 +303,7 @@
    12.4        fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
    12.5          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    12.6              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    12.7 -            ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
    12.8 +            subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
    12.9          | check _ = false
   12.10  
   12.11          fun tr' (_ $ abs) =
    13.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 16:41:22 2009 +1100
    13.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 08:16:25 2009 +0200
    13.3 @@ -124,7 +124,7 @@
    13.4        |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
    13.5      
    13.6      val tycos = map fst dataTs;
    13.7 -    val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
    13.8 +    val _ = if eq_set (op =) (tycos, raw_tycos) then ()
    13.9        else error ("Type constructors " ^ commas (map quote raw_tycos)
   13.10          ^ " do not belong exhaustively to one mutual recursive datatype");
   13.11  
   13.12 @@ -489,7 +489,7 @@
   13.13      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   13.14        let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
   13.15        in (case duplicates (op =) tvs of
   13.16 -            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   13.17 +            [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   13.18                    else error ("Mutually recursive datatypes must have same type parameters")
   13.19            | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
   13.20                " : " ^ commas dups))
    14.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Oct 21 16:41:22 2009 +1100
    14.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Oct 21 08:16:25 2009 +0200
    14.3 @@ -257,7 +257,7 @@
    14.4  fun get_nonrec_types descr sorts =
    14.5    map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
    14.6      Library.foldl (fn (Ts', (_, cargs)) =>
    14.7 -      filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
    14.8 +      union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
    14.9  
   14.10  (* get all recursive types in datatype description *)
   14.11  
    15.1 --- a/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 16:41:22 2009 +1100
    15.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 08:16:25 2009 +0200
    15.3 @@ -90,7 +90,7 @@
    15.4        IntGraph.empty
    15.5          |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
    15.6          |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
    15.7 -               if i = j orelse null (c1 inter t2) 
    15.8 +               if i = j orelse null (inter (op =) (c1, t2))
    15.9                 then I else IntGraph.add_edge_acyclic (i,j))
   15.10               num_branches num_branches
   15.11      end
    16.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 16:41:22 2009 +1100
    16.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 08:16:25 2009 +0200
    16.3 @@ -101,7 +101,7 @@
    16.4            let
    16.5              val t = Pattern.rewrite_term thy sigma [] feq1
    16.6            in
    16.7 -            fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
    16.8 +            fold_rev Logic.all (inter (op =) (map Free (frees_in_term ctx t), vs')) t
    16.9            end
   16.10      in
   16.11        map instantiate substs
    17.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 16:41:22 2009 +1100
    17.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 08:16:25 2009 +0200
    17.3 @@ -348,7 +348,7 @@
    17.4    | Add(lin1,lin2) =>
    17.5          let val lis1 = resolve_proof vars lin1
    17.6              val lis2 = resolve_proof vars lin2
    17.7 -            val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
    17.8 +            val dom = distinct (op =) (union (op =) (map fst lis1, map fst lis2))
    17.9          in
   17.10              map (fn n => let val a = these (AList.lookup (op =) lis1 n)
   17.11                               val b = these (AList.lookup (op =) lis2 n)
   17.12 @@ -884,7 +884,7 @@
   17.13   fun isolate_monomials vars tm =
   17.14   let 
   17.15    val (cmons,vmons) =
   17.16 -    List.partition (fn m => null (gen_inter op aconvc (frees m, vars)))
   17.17 +    List.partition (fn m => null (inter op aconvc (frees m, vars)))
   17.18                     (striplist ring_dest_add tm)
   17.19    val cofactors = map (fn v => find_multipliers v vmons) vars
   17.20    val cnc = if null cmons then zero_tm
    18.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 16:41:22 2009 +1100
    18.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 08:16:25 2009 +0200
    18.3 @@ -984,20 +984,20 @@
    18.4              val dupTs = map snd (duplicates (op =) vTs) @
    18.5                map_filter (AList.lookup (op =) vTs) vs;
    18.6            in
    18.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
    18.8 +            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
    18.9              forall (is_eqT o fastype_of) in_ts' andalso
   18.10 -            term_vs t subset vs andalso
   18.11 +            subset (op =) (term_vs t, vs) andalso
   18.12              forall is_eqT dupTs
   18.13            end)
   18.14              (modes_of_term modes t handle Option =>
   18.15                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   18.16        | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
   18.17              length us = length is andalso
   18.18 -            terms_vs us subset vs andalso
   18.19 -            term_vs t subset vs)
   18.20 +            subset (op =) (terms_vs us, vs) andalso
   18.21 +            subset (op =) (term_vs t, vs))
   18.22              (modes_of_term modes t handle Option =>
   18.23                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   18.24 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   18.25 +      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
   18.26            else NONE
   18.27        ) ps);
   18.28  
   18.29 @@ -1047,16 +1047,16 @@
   18.30              (if with_generator then
   18.31                (case select_mode_prem thy gen_modes' vs ps of
   18.32                  SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
   18.33 -                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   18.34 +                  (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
   18.35                    (filter_out (equal p) ps)
   18.36                | _ =>
   18.37                    let 
   18.38                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
   18.39                    in
   18.40                      case (find_first (fn generator_vs => is_some
   18.41 -                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
   18.42 +                      (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
   18.43                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
   18.44 -                        (vs union generator_vs) ps
   18.45 +                        (union (op =) (vs, generator_vs)) ps
   18.46                      | NONE => let
   18.47                      val _ = tracing ("ps:" ^ (commas
   18.48                      (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
   18.49 @@ -1065,7 +1065,7 @@
   18.50              else
   18.51                NONE)
   18.52          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
   18.53 -            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   18.54 +            (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
   18.55              (filter_out (equal p) ps))
   18.56      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
   18.57      val in_vs = terms_vs in_ts;
   18.58 @@ -1073,13 +1073,13 @@
   18.59    in
   18.60      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   18.61      forall (is_eqT o fastype_of) in_ts' then
   18.62 -      case check_mode_prems [] (param_vs union in_vs) ps of
   18.63 +      case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
   18.64           NONE => NONE
   18.65         | SOME (acc_ps, vs) =>
   18.66           if with_generator then
   18.67             SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
   18.68           else
   18.69 -           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
   18.70 +           if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
   18.71      else NONE
   18.72    end;
   18.73  
    19.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 16:41:22 2009 +1100
    19.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 08:16:25 2009 +0200
    19.3 @@ -308,7 +308,7 @@
    19.4    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
    19.5    | _ => (acc, dacc)
    19.6    val (cs,ds) = h ([],[]) p
    19.7 -  val l = Integer.lcms (cs union ds)
    19.8 +  val l = Integer.lcms (union (op =) (cs, ds))
    19.9    fun cv k ct =
   19.10      let val (tm as b$s$t) = term_of ct
   19.11      in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
    20.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Wed Oct 21 16:41:22 2009 +1100
    20.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Oct 21 08:16:25 2009 +0200
    20.3 @@ -84,7 +84,7 @@
    20.4   in h [] end;
    20.5  in 
    20.6  fun is_relevant ctxt ct = 
    20.7 - gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
    20.8 + subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
    20.9   andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
   20.10   andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
   20.11  
    21.1 --- a/src/HOL/Tools/TFL/post.ML	Wed Oct 21 16:41:22 2009 +1100
    21.2 +++ b/src/HOL/Tools/TFL/post.ML	Wed Oct 21 08:16:25 2009 +0200
    21.3 @@ -28,7 +28,7 @@
    21.4   *--------------------------------------------------------------------------*)
    21.5  fun termination_goals rules =
    21.6      map (Type.freeze o HOLogic.dest_Trueprop)
    21.7 -      (List.foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
    21.8 +      (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules);
    21.9  
   21.10  (*---------------------------------------------------------------------------
   21.11   * Three postprocessors are applied to the definition.  It
   21.12 @@ -79,7 +79,7 @@
   21.13        val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   21.14        val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   21.15        val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   21.16 -      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
   21.17 +      val cntxt = union (op aconv) (cntxtl, cntxtr)
   21.18    in
   21.19      R.GEN_ALL
   21.20        (R.DISCH_ALL
    22.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 16:41:22 2009 +1100
    22.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 08:16:25 2009 +0200
    22.3 @@ -531,7 +531,7 @@
    22.4                   then writeln (cat_lines ("Extractants =" ::
    22.5                    map (Display.string_of_thm_global thy) extractants))
    22.6                   else ()
    22.7 -     val TCs = List.foldr (gen_union (op aconv)) [] TCl
    22.8 +     val TCs = List.foldr (union (op aconv)) [] TCl
    22.9       val full_rqt = WFR::TCs
   22.10       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   22.11       val R'abs = S.rand R'
    23.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 16:41:22 2009 +1100
    23.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 08:16:25 2009 +0200
    23.3 @@ -202,15 +202,15 @@
    23.4              val dupTs = map snd (duplicates (op =) vTs) @
    23.5                map_filter (AList.lookup (op =) vTs) vs;
    23.6            in
    23.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
    23.8 +            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
    23.9              forall (is_eqT o fastype_of) in_ts' andalso
   23.10 -            term_vs t subset vs andalso
   23.11 +            subset (op =) (term_vs t, vs) andalso
   23.12              forall is_eqT dupTs
   23.13            end)
   23.14              (if is_set then [Mode (([], []), [], [])]
   23.15               else modes_of modes t handle Option =>
   23.16                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   23.17 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   23.18 +      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
   23.19            else NONE) ps);
   23.20  
   23.21  fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
   23.22 @@ -222,7 +222,7 @@
   23.23        | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
   23.24            NONE => NONE
   23.25          | SOME (x, _) => check_mode_prems
   23.26 -            (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
   23.27 +            (case x of Prem (us, _, _) => union (op =) (vs, terms_vs us) | _ => vs)
   23.28              (filter_out (equal x) ps));
   23.29      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
   23.30      val in_vs = terms_vs in_ts;
   23.31 @@ -230,9 +230,9 @@
   23.32    in
   23.33      forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   23.34      forall (is_eqT o fastype_of) in_ts' andalso
   23.35 -    (case check_mode_prems (arg_vs union in_vs) ps of
   23.36 +    (case check_mode_prems (union (op =) (arg_vs, in_vs)) ps of
   23.37         NONE => false
   23.38 -     | SOME vs => concl_vs subset vs)
   23.39 +     | SOME vs => subset (op =) (concl_vs, vs))
   23.40    end;
   23.41  
   23.42  fun check_modes_pred thy arg_vs preds modes (p, ms) =
   23.43 @@ -482,7 +482,7 @@
   23.44  fun constrain cs [] = []
   23.45    | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
   23.46        NONE => xs
   23.47 -    | SOME xs' => xs inter xs') :: constrain cs ys;
   23.48 +    | SOME xs' => inter (op =) (xs, xs')) :: constrain cs ys;
   23.49  
   23.50  fun mk_extra_defs thy defs gr dep names module ts =
   23.51    Library.foldl (fn (gr, name) =>
    24.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Oct 21 16:41:22 2009 +1100
    24.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 21 08:16:25 2009 +0200
    24.3 @@ -209,7 +209,7 @@
    24.4        (case optf of
    24.5           NONE => fs
    24.6         | SOME f => AList.update op = (u, the_default f
    24.7 -           (Option.map (curry op inter f) (AList.lookup op = fs u))) fs));
    24.8 +           (Option.map (curry (inter (op =)) f) (AList.lookup op = fs u))) fs));
    24.9  
   24.10  
   24.11  (**************************************************************)
    25.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Oct 21 16:41:22 2009 +1100
    25.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 21 08:16:25 2009 +0200
    25.3 @@ -631,7 +631,7 @@
    25.4          let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
    25.5          in
    25.6             {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
    25.7 -            tfrees = tfree_lits union tfrees}
    25.8 +            tfrees = union (op =) (tfree_lits, tfrees)}
    25.9          end;
   25.10        val lmap0 = List.foldl (add_thm true)
   25.11                          {axioms = [], tfrees = init_tfrees ctxt} cls
    26.1 --- a/src/HOL/Tools/old_primrec.ML	Wed Oct 21 16:41:22 2009 +1100
    26.2 +++ b/src/HOL/Tools/old_primrec.ML	Wed Oct 21 08:16:25 2009 +0200
    26.3 @@ -226,7 +226,7 @@
    26.4        (case Symtab.lookup dt_info tname of
    26.5            NONE => primrec_err (quote tname ^ " is not a datatype")
    26.6          | SOME dt =>
    26.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
    26.8 +            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
    26.9                (tname, dt)::(find_dts dt_info tnames' tnames)
   26.10              else find_dts dt_info tnames' tnames);
   26.11  
   26.12 @@ -265,7 +265,7 @@
   26.13      val defs' = map (make_def thy fs) defs;
   26.14      val nameTs1 = map snd fnameTs;
   26.15      val nameTs2 = map fst rec_eqns;
   26.16 -    val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
   26.17 +    val _ = if eq_set (op =) (nameTs1, nameTs2) then ()
   26.18              else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
   26.19                "\nare not mutually recursive");
   26.20      val primrec_name =
    27.1 --- a/src/HOL/Tools/primrec.ML	Wed Oct 21 16:41:22 2009 +1100
    27.2 +++ b/src/HOL/Tools/primrec.ML	Wed Oct 21 08:16:25 2009 +0200
    27.3 @@ -208,7 +208,7 @@
    27.4        (case Symtab.lookup dt_info tname of
    27.5            NONE => primrec_error (quote tname ^ " is not a datatype")
    27.6          | SOME dt =>
    27.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
    27.8 +            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
    27.9                (tname, dt)::(find_dts dt_info tnames' tnames)
   27.10              else find_dts dt_info tnames' tnames);
   27.11  
   27.12 @@ -232,7 +232,7 @@
   27.13      val defs = map (make_def lthy fixes fs) raw_defs;
   27.14      val names = map snd fnames;
   27.15      val names_eqns = map fst eqns;
   27.16 -    val _ = if gen_eq_set (op =) (names, names_eqns) then ()
   27.17 +    val _ = if eq_set (op =) (names, names_eqns) then ()
   27.18        else primrec_error ("functions " ^ commas_quote names_eqns ^
   27.19          "\nare not mutually recursive");
   27.20      val rec_rewrites' = map mk_meta_eq rec_rewrites;
    28.1 --- a/src/HOL/Tools/prop_logic.ML	Wed Oct 21 16:41:22 2009 +1100
    28.2 +++ b/src/HOL/Tools/prop_logic.ML	Wed Oct 21 08:16:25 2009 +0200
    28.3 @@ -111,8 +111,8 @@
    28.4  	  | indices False            = []
    28.5  	  | indices (BoolVar i)      = [i]
    28.6  	  | indices (Not fm)         = indices fm
    28.7 -	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
    28.8 -	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
    28.9 +	  | indices (Or (fm1, fm2))  = union (op =) (indices fm1, indices fm2)
   28.10 +	  | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2);
   28.11  
   28.12  (* ------------------------------------------------------------------------- *)
   28.13  (* maxidx: computes the maximal variable index occuring in a formula of      *)
    29.1 --- a/src/HOL/Tools/record.ML	Wed Oct 21 16:41:22 2009 +1100
    29.2 +++ b/src/HOL/Tools/record.ML	Wed Oct 21 08:16:25 2009 +0200
    29.3 @@ -1834,7 +1834,7 @@
    29.4      val extN = full bname;
    29.5      val types = map snd fields;
    29.6      val alphas_fields = fold Term.add_tfree_namesT types [];
    29.7 -    val alphas_ext = alphas inter alphas_fields;
    29.8 +    val alphas_ext = inter (op =) (alphas, alphas_fields);
    29.9      val len = length fields;
   29.10      val variants =
   29.11        Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
    30.1 --- a/src/HOL/Tools/refute.ML	Wed Oct 21 16:41:22 2009 +1100
    30.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 21 08:16:25 2009 +0200
    30.3 @@ -1154,7 +1154,7 @@
    30.4        val axioms = collect_axioms thy u
    30.5        (* Term.typ list *)
    30.6        val types = Library.foldl (fn (acc, t') =>
    30.7 -        acc union (ground_types thy t')) ([], u :: axioms)
    30.8 +        union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
    30.9        val _     = tracing ("Ground types: "
   30.10          ^ (if null types then "none."
   30.11             else commas (map (Syntax.string_of_typ_global thy) types)))
   30.12 @@ -2415,7 +2415,7 @@
   30.13                        (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
   30.14                    (* sanity check: typ_assoc must associate types to the   *)
   30.15                    (*               elements of 'dtyps' (and only to those) *)
   30.16 -                  val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
   30.17 +                  val _ = if not (eq_set (op =) (dtyps, map fst typ_assoc))
   30.18                      then
   30.19                        raise REFUTE ("IDT_recursion_interpreter",
   30.20                          "type association has extra/missing elements")
   30.21 @@ -3007,7 +3007,7 @@
   30.22          [Type ("fun", [T, Type ("bool", [])]),
   30.23           Type ("fun", [_, Type ("bool", [])])]),
   30.24           Type ("fun", [_, Type ("bool", [])])])) =>
   30.25 -      let nonfix union (* because "union" is used below *)
   30.26 +      let
   30.27          val size_elem = size_of_type thy model T
   30.28          (* the universe (i.e. the set that contains every element) *)
   30.29          val i_univ = Node (replicate size_elem TT)
    31.1 --- a/src/HOL/Tools/res_atp.ML	Wed Oct 21 16:41:22 2009 +1100
    31.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Oct 21 08:16:25 2009 +0200
    31.3 @@ -211,8 +211,9 @@
    31.4          fun defs lhs rhs =
    31.5              let val (rator,args) = strip_comb lhs
    31.6                  val ct = const_with_typ thy (dest_ConstFree rator)
    31.7 -            in  forall is_Var args andalso uni_mem gctypes ct andalso
    31.8 -                Term.add_vars rhs [] subset Term.add_vars lhs []
    31.9 +            in
   31.10 +              forall is_Var args andalso uni_mem gctypes ct andalso
   31.11 +                subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
   31.12              end
   31.13              handle ConstFree => false
   31.14      in    
    32.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Oct 21 16:41:22 2009 +1100
    32.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Oct 21 08:16:25 2009 +0200
    32.3 @@ -473,7 +473,7 @@
    32.4        val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
    32.5                                        (map Thm.term_of hyps)
    32.6        val fixed = OldTerm.term_frees (concl_of st) @
    32.7 -                  List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
    32.8 +                  List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
    32.9    in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   32.10  
   32.11  
    33.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 21 16:41:22 2009 +1100
    33.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 21 08:16:25 2009 +0200
    33.3 @@ -93,7 +93,7 @@
    33.4  val tconst_prefix = "tc_";
    33.5  val class_prefix = "class_";
    33.6  
    33.7 -fun union_all xss = List.foldl (op union) [] xss;
    33.8 +fun union_all xss = List.foldl (union (op =)) [] xss;
    33.9  
   33.10  (*Provide readable names for the more common symbolic functions*)
   33.11  val const_trans_table =
   33.12 @@ -263,7 +263,7 @@
   33.13    | pred_of_sort (LTFree (s,ty)) = (s,1)
   33.14  
   33.15  (*Given a list of sorted type variables, return a list of type literals.*)
   33.16 -fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts);
   33.17 +fun add_typs Ts = List.foldl (union (op =)) [] (map sorts_on_typs Ts);
   33.18  
   33.19  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   33.20    * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   33.21 @@ -372,7 +372,7 @@
   33.22        let val cpairs = type_class_pairs thy tycons classes
   33.23            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
   33.24            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   33.25 -      in  (classes' union classes, cpairs' union cpairs)  end;
   33.26 +      in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;
   33.27  
   33.28  fun make_arity_clauses_dfg dfg thy tycons classes =
   33.29    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
    34.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 16:41:22 2009 +1100
    34.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 08:16:25 2009 +0200
    34.3 @@ -155,7 +155,7 @@
    34.4    | combterm_of dfg thy (P $ Q) =
    34.5        let val (P',tsP) = combterm_of dfg thy P
    34.6            val (Q',tsQ) = combterm_of dfg thy Q
    34.7 -      in  (CombApp(P',Q'), tsP union tsQ)  end
    34.8 +      in  (CombApp(P',Q'), union (op =) (tsP, tsQ))  end
    34.9    | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
   34.10  
   34.11  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
   34.12 @@ -167,7 +167,7 @@
   34.13    | literals_of_term1 dfg thy (lits,ts) P =
   34.14        let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   34.15        in
   34.16 -          (Literal(pol,pred)::lits, ts union ts')
   34.17 +          (Literal(pol,pred)::lits, union (op =) (ts, ts'))
   34.18        end;
   34.19  
   34.20  fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   34.21 @@ -476,7 +476,7 @@
   34.22      val (cma, cnh) = count_constants clauses
   34.23      val params = (t_full, cma, cnh)
   34.24      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   34.25 -    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
   34.26 +    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (union (op =)) [] tfree_litss)
   34.27      val _ =
   34.28        File.write_list file (
   34.29          map (#1 o (clause2tptp params)) axclauses @
    35.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 16:41:22 2009 +1100
    35.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 08:16:25 2009 +0200
    35.3 @@ -364,7 +364,7 @@
    35.4  fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
    35.5  
    35.6  fun replace_deps (old:int, new) (lno, t, deps) =
    35.7 -      (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps));
    35.8 +      (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps));
    35.9  
   35.10  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   35.11    only in type information.*)
    36.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 16:41:22 2009 +1100
    36.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 08:16:25 2009 +0200
    36.3 @@ -471,8 +471,8 @@
    36.4          | forced_vars False             = []
    36.5          | forced_vars (BoolVar i)       = [i]
    36.6          | forced_vars (Not (BoolVar i)) = [~i]
    36.7 -        | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
    36.8 -        | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
    36.9 +        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1, forced_vars fm2)
   36.10 +        | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1, forced_vars fm2)
   36.11          (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   36.12          (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   36.13          | forced_vars _                 = error "formula is not in negation normal form"
    37.1 --- a/src/HOL/Tools/transfer.ML	Wed Oct 21 16:41:22 2009 +1100
    37.2 +++ b/src/HOL/Tools/transfer.ML	Wed Oct 21 08:16:25 2009 +0200
    37.3 @@ -143,7 +143,7 @@
    37.4   {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
    37.5    ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
    37.6    hints = subtract (op = : string*string -> bool) hints0
    37.7 -            (hints1 union_string hints2)}
    37.8 +            (union (op =) (hints1, hints2))}
    37.9   end;
   37.10  
   37.11  local
   37.12 @@ -151,7 +151,7 @@
   37.13  in
   37.14  fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
   37.15                     {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
   37.16 -    {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}
   37.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)}
   37.18  end;
   37.19  
   37.20  fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
    38.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Oct 21 16:41:22 2009 +1100
    38.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Oct 21 08:16:25 2009 +0200
    38.3 @@ -908,20 +908,20 @@
    38.4              val dupTs = map snd (duplicates (op =) vTs) @
    38.5                map_filter (AList.lookup (op =) vTs) vs;
    38.6            in
    38.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
    38.8 +            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
    38.9              forall (is_eqT o fastype_of) in_ts' andalso
   38.10 -            term_vs t subset vs andalso
   38.11 +            subset (op =) (term_vs t, vs) andalso
   38.12              forall is_eqT dupTs
   38.13            end)
   38.14              (modes_of_term modes t handle Option =>
   38.15                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   38.16        | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
   38.17              length us = length is andalso
   38.18 -            terms_vs us subset vs andalso
   38.19 -            term_vs t subset vs)
   38.20 +            subset (op =) (terms_vs us, vs) andalso
   38.21 +            subset (op =) (term_vs t, vs)
   38.22              (modes_of_term modes t handle Option =>
   38.23                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   38.24 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   38.25 +      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
   38.26            else NONE
   38.27        ) ps);
   38.28  
   38.29 @@ -964,22 +964,22 @@
   38.30              (if with_generator then
   38.31                (case select_mode_prem thy gen_modes' vs ps of
   38.32                    SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
   38.33 -                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   38.34 +                  (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
   38.35                    (filter_out (equal p) ps)
   38.36                  | NONE =>
   38.37                    let 
   38.38                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
   38.39                    in
   38.40                      case (find_first (fn generator_vs => is_some
   38.41 -                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
   38.42 +                      (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
   38.43                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
   38.44 -                        (vs union generator_vs) ps
   38.45 +                        (union (op =) (vs, generator_vs)) ps
   38.46                      | NONE => NONE
   38.47                    end)
   38.48              else
   38.49                NONE)
   38.50          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
   38.51 -            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   38.52 +            (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
   38.53              (filter_out (equal p) ps))
   38.54      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
   38.55      val in_vs = terms_vs in_ts;
   38.56 @@ -987,13 +987,13 @@
   38.57    in
   38.58      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   38.59      forall (is_eqT o fastype_of) in_ts' then
   38.60 -      case check_mode_prems [] (param_vs union in_vs) ps of
   38.61 +      case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
   38.62           NONE => NONE
   38.63         | SOME (acc_ps, vs) =>
   38.64           if with_generator then
   38.65             SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
   38.66           else
   38.67 -           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
   38.68 +           if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
   38.69      else NONE
   38.70    end;
   38.71  
    39.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Oct 21 16:41:22 2009 +1100
    39.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Oct 21 08:16:25 2009 +0200
    39.3 @@ -59,8 +59,8 @@
    39.4              fun analyse indirect (TFree(v,s))  =
    39.5                  (case AList.lookup (op =) tvars v of 
    39.6                     NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
    39.7 -                 | SOME sort => if eq_set_string (s,defaultS) orelse
    39.8 -                                   eq_set_string (s,sort    )
    39.9 +                 | SOME sort => if eq_set (op =) (s, defaultS) orelse
   39.10 +                                   eq_set (op =) (s, sort)
   39.11                                  then TFree(v,sort)
   39.12                                  else error ("Inconsistent sort constraint" ^
   39.13                                              " for type variable " ^ quote v))
    40.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 16:41:22 2009 +1100
    40.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 08:16:25 2009 +0200
    40.3 @@ -74,7 +74,7 @@
    40.4  fun proc ss t =
    40.5    let val (divs,mods) = coll_div_mod t ([],[])
    40.6    in if null divs orelse null mods then NONE
    40.7 -     else case divs inter mods of
    40.8 +     else case inter (op =) (divs, mods) of
    40.9              pq :: _ => SOME (cancel ss t pq)
   40.10            | [] => NONE
   40.11    end
    41.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Oct 21 16:41:22 2009 +1100
    41.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Oct 21 08:16:25 2009 +0200
    41.3 @@ -385,7 +385,7 @@
    41.4    let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
    41.5    if not (null eqs) then
    41.6       let val c =
    41.7 -           fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs []
    41.8 +           fold (fn Lineq(_,_,l,_) => fn cs => union (op =) (l, cs)) eqs []
    41.9             |> filter (fn i => i <> 0)
   41.10             |> sort (int_ord o pairself abs)
   41.11             |> hd
   41.12 @@ -429,8 +429,8 @@
   41.13  val warning_count = Unsynchronized.ref 0;
   41.14  val warning_count_max = 10;
   41.15  
   41.16 -val union_term = curry (gen_union Pattern.aeconv);
   41.17 -val union_bterm = curry (gen_union
   41.18 +val union_term = curry (union Pattern.aeconv);
   41.19 +val union_bterm = curry (union
   41.20    (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
   41.21  
   41.22  fun add_atoms (lhs, _, _, rhs, _, _) =
    42.1 --- a/src/Pure/General/name_space.ML	Wed Oct 21 16:41:22 2009 +1100
    42.2 +++ b/src/Pure/General/name_space.ML	Wed Oct 21 08:16:25 2009 +0200
    42.3 @@ -145,7 +145,7 @@
    42.4        space
    42.5        |> add_name' name name
    42.6        |> fold (del_name name)
    42.7 -        (if fully then names else names inter_string [Long_Name.base_name name])
    42.8 +        (if fully then names else inter (op =) (names, [Long_Name.base_name name]))
    42.9        |> fold (del_name_extra name) (get_accesses space name)
   42.10      end;
   42.11  
    43.1 --- a/src/Pure/General/ord_list.ML	Wed Oct 21 16:41:22 2009 +1100
    43.2 +++ b/src/Pure/General/ord_list.ML	Wed Oct 21 08:16:25 2009 +0200
    43.3 @@ -56,7 +56,6 @@
    43.4  
    43.5  (* lists as sets *)
    43.6  
    43.7 -nonfix subset;
    43.8  fun subset ord (list1, list2) =
    43.9    let
   43.10      fun sub [] _ = true
   43.11 @@ -75,7 +74,6 @@
   43.12  fun handle_same f x = f x handle SAME => x;
   43.13  
   43.14  (*union: insert elements of first list into second list*)
   43.15 -nonfix union;
   43.16  fun union ord list1 list2 =
   43.17    let
   43.18      fun unio [] _ = raise SAME
   43.19 @@ -88,7 +86,6 @@
   43.20    in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
   43.21  
   43.22  (*intersection: filter second list for elements present in first list*)
   43.23 -nonfix inter;
   43.24  fun inter ord list1 list2 =
   43.25    let
   43.26      fun intr _ [] = raise SAME
    44.1 --- a/src/Pure/General/path.ML	Wed Oct 21 16:41:22 2009 +1100
    44.2 +++ b/src/Pure/General/path.ML	Wed Oct 21 08:16:25 2009 +0200
    44.3 @@ -42,7 +42,7 @@
    44.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
    44.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    44.6    | check_elem chs =
    44.7 -      (case ["/", "\\", "$", ":"] inter_string chs of
    44.8 +      (case inter (op =) (["/", "\\", "$", ":"], chs) of
    44.9          [] => chs
   44.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
   44.11  
    45.1 --- a/src/Pure/Proof/extraction.ML	Wed Oct 21 16:41:22 2009 +1100
    45.2 +++ b/src/Pure/Proof/extraction.ML	Wed Oct 21 08:16:25 2009 +0200
    45.3 @@ -198,7 +198,7 @@
    45.4      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
    45.5       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    45.6       types = AList.merge (op =) (K true) (types1, types2),
    45.7 -     realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
    45.8 +     realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
    45.9       defs = Library.merge Thm.eq_thm (defs1, defs2),
   45.10       expand = Library.merge (op =) (expand1, expand2),
   45.11       prep = (case prep1 of NONE => prep2 | _ => prep1)};
   45.12 @@ -468,7 +468,7 @@
   45.13  
   45.14        in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
   45.15  
   45.16 -    fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
   45.17 +    fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
   45.18      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
   45.19  
   45.20      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
    46.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Oct 21 16:41:22 2009 +1100
    46.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Oct 21 08:16:25 2009 +0200
    46.3 @@ -289,7 +289,7 @@
    46.4      val _ = message "Collecting constraints...";
    46.5      val (t, prf, cs, env, _) = make_constraints_cprf thy
    46.6        (Envir.empty (maxidx_proof cprf ~1)) cprf';
    46.7 -    val cs' = map (fn p => (true, p, op union
    46.8 +    val cs' = map (fn p => (true, p, union (op =) 
    46.9          (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
   46.10        (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
   46.11      val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
    47.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Oct 21 16:41:22 2009 +1100
    47.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Oct 21 08:16:25 2009 +0200
    47.3 @@ -77,7 +77,7 @@
    47.4    |> command K.prf_asm_goal     goal
    47.5    |> command K.prf_script       proofstep;
    47.6  
    47.7 -val _ = OuterKeyword.kinds subset_string Symtab.keys command_keywords
    47.8 +val _ = subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
    47.9    orelse sys_error "Incomplete coverage of command keywords";
   47.10  
   47.11  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    48.1 --- a/src/Pure/Syntax/ast.ML	Wed Oct 21 16:41:22 2009 +1100
    48.2 +++ b/src/Pure/Syntax/ast.ML	Wed Oct 21 08:16:25 2009 +0200
    48.3 @@ -104,7 +104,7 @@
    48.4      val rvars = add_vars rhs [];
    48.5    in
    48.6      if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
    48.7 -    else if not (rvars subset lvars) then SOME "rhs contains extra variables"
    48.8 +    else if not (subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
    48.9      else NONE
   48.10    end;
   48.11  
    49.1 --- a/src/Pure/Syntax/parser.ML	Wed Oct 21 16:41:22 2009 +1100
    49.2 +++ b/src/Pure/Syntax/parser.ML	Wed Oct 21 08:16:25 2009 +0200
    49.3 @@ -101,7 +101,7 @@
    49.4  
    49.5              val tos = connected_with chains' [lhs] [lhs];
    49.6          in (copy_lookahead tos [],
    49.7 -            gen_union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
    49.8 +            union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
    49.9          end;
   49.10  
   49.11        (*test if new production can produce lambda
   49.12 @@ -109,7 +109,7 @@
   49.13        val (new_lambda, lambdas') =
   49.14          if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
   49.15                      | (Terminal _) => false) rhs then
   49.16 -          (true, gen_union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
   49.17 +          (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
   49.18          else
   49.19            (false, lambdas');
   49.20  
   49.21 @@ -125,7 +125,7 @@
   49.22        (*get all known starting tokens for a nonterminal*)
   49.23        fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
   49.24  
   49.25 -      val token_union = gen_union matching_tokens;
   49.26 +      val token_union = union matching_tokens;
   49.27  
   49.28        (*update prods, lookaheads, and lambdas according to new lambda NTs*)
   49.29        val (added_starts', lambdas') =
   49.30 @@ -147,7 +147,7 @@
   49.31                      in
   49.32                        if member (op =) nts l then       (*update production's lookahead*)
   49.33                        let
   49.34 -                        val new_lambda = is_none tk andalso nts subset lambdas;
   49.35 +                        val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
   49.36  
   49.37                          val new_tks = subtract (op =) l_starts
   49.38                            ((if is_some tk then [the tk] else []) @
   49.39 @@ -155,7 +155,7 @@
   49.40  
   49.41                          val added_tks' = token_union (new_tks, added_tks);
   49.42  
   49.43 -                        val nt_dependencies' = gen_union (op =) (nts, nt_dependencies);
   49.44 +                        val nt_dependencies' = union (op =) (nts, nt_dependencies);
   49.45  
   49.46                          (*associate production with new starting tokens*)
   49.47                          fun copy ([]: token option list) nt_prods = nt_prods
   49.48 @@ -413,7 +413,7 @@
   49.49          fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
   49.50  
   49.51          val nt_prods =
   49.52 -          Library.foldl (gen_union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
   49.53 +          Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
   49.54            map prod_of_chain ((these o AList.lookup (op =) chains) tag);
   49.55        in map (pretty_prod name) nt_prods end;
   49.56  
   49.57 @@ -562,7 +562,7 @@
   49.58      fun process_nt ~1 result = result
   49.59        | process_nt nt result =
   49.60          let
   49.61 -          val nt_prods = Library.foldl (gen_union op =)
   49.62 +          val nt_prods = Library.foldl (union op =)
   49.63                               ([], map snd (snd (Array.sub (prods2, nt))));
   49.64            val lhs_tag = convert_tag nt;
   49.65  
    50.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Oct 21 16:41:22 2009 +1100
    50.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Oct 21 08:16:25 2009 +0200
    50.3 @@ -352,7 +352,7 @@
    50.4    in
    50.5      SynExt {
    50.6        xprods = xprods,
    50.7 -      consts = consts union_string mfix_consts,
    50.8 +      consts = union (op =) (consts, mfix_consts),
    50.9        prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
   50.10        parse_ast_translation = parse_ast_translation,
   50.11        parse_rules = parse_rules' @ parse_rules,
    51.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Oct 21 16:41:22 2009 +1100
    51.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 21 08:16:25 2009 +0200
    51.3 @@ -248,7 +248,7 @@
    51.4  
    51.5      fun check (t, NONE) = check (t, SOME (get_thm_names t))
    51.6        | check ((_, thm), c as SOME thm_consts) =
    51.7 -         (if pat_consts subset_string thm_consts andalso
    51.8 +         (if subset (op =) (pat_consts, thm_consts) andalso
    51.9              Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
   51.10            then SOME (0, 0) else NONE, c);
   51.11    in check end;
    52.1 --- a/src/Pure/codegen.ML	Wed Oct 21 16:41:22 2009 +1100
    52.2 +++ b/src/Pure/codegen.ML	Wed Oct 21 08:16:25 2009 +0200
    52.3 @@ -599,8 +599,8 @@
    52.4       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
    52.5  
    52.6  fun new_names t xs = Name.variant_list
    52.7 -  (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
    52.8 -    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
    52.9 +  (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
   52.10 +    OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
   52.11  
   52.12  fun new_name t x = hd (new_names t [x]);
   52.13  
    53.1 --- a/src/Pure/library.ML	Wed Oct 21 16:41:22 2009 +1100
    53.2 +++ b/src/Pure/library.ML	Wed Oct 21 08:16:25 2009 +0200
    53.3 @@ -11,8 +11,7 @@
    53.4  infix 2 ?
    53.5  infix 3 o oo ooo oooo
    53.6  infix 4 ~~ upto downto
    53.7 -infix orf andf \ \\ mem mem_int mem_string union union_int
    53.8 -  union_string inter inter_int inter_string subset subset_int subset_string
    53.9 +infix orf andf \ \\ mem mem_int mem_string
   53.10  
   53.11  signature BASIC_LIBRARY =
   53.12  sig
   53.13 @@ -163,21 +162,10 @@
   53.14    val mem: ''a * ''a list -> bool
   53.15    val mem_int: int * int list -> bool
   53.16    val mem_string: string * string list -> bool
   53.17 -  val union: ''a list * ''a list -> ''a list
   53.18 -  val union_int: int list * int list -> int list
   53.19 -  val union_string: string list * string list -> string list
   53.20 -  val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   53.21 -  val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   53.22 -  val inter: ''a list * ''a list -> ''a list
   53.23 -  val inter_int: int list * int list -> int list
   53.24 -  val inter_string: string list * string list -> string list
   53.25 -  val subset: ''a list * ''a list -> bool
   53.26 -  val subset_int: int list * int list -> bool
   53.27 -  val subset_string: string list * string list -> bool
   53.28 -  val eq_set: ''a list * ''a list -> bool
   53.29 -  val eq_set_string: string list * string list -> bool
   53.30 -  val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   53.31 -  val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   53.32 +  val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   53.33 +  val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   53.34 +  val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   53.35 +  val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   53.36    val \ : ''a list * ''a -> ''a list
   53.37    val \\ : ''a list * ''a list -> ''a list
   53.38    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   53.39 @@ -811,73 +799,23 @@
   53.40  fun (x: string) mem_string xs = member (op =) xs x;
   53.41  
   53.42  (*union of sets represented as lists: no repetitions*)
   53.43 -fun xs union [] = xs
   53.44 -  | [] union ys = ys
   53.45 -  | (x :: xs) union ys = xs union (insert (op =) x ys);
   53.46 -
   53.47 -(*union of sets, optimized version for ints*)
   53.48 -fun (xs:int list) union_int [] = xs
   53.49 -  | [] union_int ys = ys
   53.50 -  | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
   53.51 -
   53.52 -(*union of sets, optimized version for strings*)
   53.53 -fun (xs:string list) union_string [] = xs
   53.54 -  | [] union_string ys = ys
   53.55 -  | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
   53.56 -
   53.57 -(*generalized union*)
   53.58 -fun gen_union eq (xs, []) = xs
   53.59 -  | gen_union eq ([], ys) = ys
   53.60 -  | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
   53.61 -
   53.62 +fun union eq (xs, []) = xs
   53.63 +  | union eq ([], ys) = ys
   53.64 +  | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
   53.65  
   53.66  (*intersection*)
   53.67 -fun [] inter ys = []
   53.68 -  | (x :: xs) inter ys =
   53.69 -      if x mem ys then x :: (xs inter ys) else xs inter ys;
   53.70 -
   53.71 -(*intersection, optimized version for ints*)
   53.72 -fun ([]:int list) inter_int ys = []
   53.73 -  | (x :: xs) inter_int ys =
   53.74 -      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
   53.75 -
   53.76 -(*intersection, optimized version for strings *)
   53.77 -fun ([]:string list) inter_string ys = []
   53.78 -  | (x :: xs) inter_string ys =
   53.79 -      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
   53.80 -
   53.81 -(*generalized intersection*)
   53.82 -fun gen_inter eq ([], ys) = []
   53.83 -  | gen_inter eq (x::xs, ys) =
   53.84 -      if member eq ys x then x :: gen_inter eq (xs, ys)
   53.85 -      else gen_inter eq (xs, ys);
   53.86 -
   53.87 +fun inter eq ([], ys) = []
   53.88 +  | inter eq (x::xs, ys) =
   53.89 +      if member eq ys x then x :: inter eq (xs, ys)
   53.90 +      else inter eq (xs, ys);
   53.91  
   53.92  (*subset*)
   53.93 -fun [] subset ys = true
   53.94 -  | (x :: xs) subset ys = x mem ys andalso xs subset ys;
   53.95 -
   53.96 -(*subset, optimized version for ints*)
   53.97 -fun ([]: int list) subset_int ys = true
   53.98 -  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
   53.99 -
  53.100 -(*subset, optimized version for strings*)
  53.101 -fun ([]: string list) subset_string ys = true
  53.102 -  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
  53.103 +fun subset eq (xs, ys) = forall (member eq ys) xs;
  53.104  
  53.105  (*set equality*)
  53.106 -fun eq_set (xs, ys) =
  53.107 -  xs = ys orelse (xs subset ys andalso ys subset xs);
  53.108 -
  53.109 -(*set equality for strings*)
  53.110 -fun eq_set_string ((xs: string list), ys) =
  53.111 -  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
  53.112 -
  53.113 -fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
  53.114 -
  53.115 -fun gen_eq_set eq (xs, ys) =
  53.116 +fun eq_set eq (xs, ys) =
  53.117    eq_list eq (xs, ys) orelse
  53.118 -    (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
  53.119 +    (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
  53.120  
  53.121  
  53.122  (*removing an element from a list WITHOUT duplicates*)
    54.1 --- a/src/Pure/meta_simplifier.ML	Wed Oct 21 16:41:22 2009 +1100
    54.2 +++ b/src/Pure/meta_simplifier.ML	Wed Oct 21 08:16:25 2009 +0200
    54.3 @@ -398,7 +398,7 @@
    54.4    | vperm (t, u) = (t = u);
    54.5  
    54.6  fun var_perm (t, u) =
    54.7 -  vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
    54.8 +  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
    54.9  
   54.10  (*simple test for looping rewrite rules and stupid orientations*)
   54.11  fun default_reorient thy prems lhs rhs =
   54.12 @@ -864,7 +864,7 @@
   54.13    while the premises are solved.*)
   54.14  
   54.15  fun cond_skel (args as (_, (lhs, rhs))) =
   54.16 -  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
   54.17 +  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
   54.18    else skel0;
   54.19  
   54.20  (*
    55.1 --- a/src/Pure/pattern.ML	Wed Oct 21 16:41:22 2009 +1100
    55.2 +++ b/src/Pure/pattern.ML	Wed Oct 21 08:16:25 2009 +0200
    55.3 @@ -216,10 +216,10 @@
    55.4  
    55.5  fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
    55.6    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    55.7 -            if js subset_int is
    55.8 +            if subset (op =) (js, is)
    55.9              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
   55.10                   in Envir.update (((F, Fty), t), env) end
   55.11 -            else let val ks = is inter_int js
   55.12 +            else let val ks = inter (op =) (is, js)
   55.13                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
   55.14                       val (env',H) = Envir.genvar a (env,Hty)
   55.15                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
   55.16 @@ -339,7 +339,7 @@
   55.17    let val js = loose_bnos t
   55.18    in if null is
   55.19       then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
   55.20 -     else if js subset_int is
   55.21 +     else if subset (op =) (js, is)
   55.22            then let val t' = if downto0(is,length binders - 1) then t
   55.23                              else mapbnd (idx is) t
   55.24                 in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end
    56.1 --- a/src/Pure/proofterm.ML	Wed Oct 21 16:41:22 2009 +1100
    56.2 +++ b/src/Pure/proofterm.ML	Wed Oct 21 08:16:25 2009 +0200
    56.3 @@ -900,8 +900,8 @@
    56.4  
    56.5  fun add_funvars Ts (vs, t) =
    56.6    if is_fun (fastype_of1 (Ts, t)) then
    56.7 -    vs union map_filter (fn Var (ixn, T) =>
    56.8 -      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)
    56.9 +    union (op =) (vs, map_filter (fn Var (ixn, T) =>
   56.10 +      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
   56.11    else vs;
   56.12  
   56.13  fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
   56.14 @@ -918,7 +918,7 @@
   56.15    | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   56.16    | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
   56.17  
   56.18 -fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
   56.19 +fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P, prop_vars Q)
   56.20    | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
   56.21    | prop_vars t = (case strip_comb t of
   56.22        (Var (ixn, _), _) => [ixn] | _ => []);
   56.23 @@ -936,9 +936,9 @@
   56.24    end;
   56.25  
   56.26  fun needed_vars prop =
   56.27 -  Library.foldl (op union)
   56.28 -    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
   56.29 -  prop_vars prop;
   56.30 +  union (op =) (Library.foldl (union (op =))
   56.31 +    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
   56.32 +  prop_vars prop);
   56.33  
   56.34  fun gen_axm_proof c name prop =
   56.35    let
   56.36 @@ -975,7 +975,7 @@
   56.37            let
   56.38              val p as (_, is', ch', prf') = shrink ls lev prf2;
   56.39              val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
   56.40 -          in (is union is', ch orelse ch', ts',
   56.41 +          in (union (op =) (is, is'), ch orelse ch', ts',
   56.42                if ch orelse ch' then prf'' %% prf' else prf)
   56.43            end
   56.44        | shrink' ls lev ts prfs (prf as prf1 % t) =
   56.45 @@ -1004,15 +1004,15 @@
   56.46              val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
   56.47              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
   56.48                insert (op =) ixn (case AList.lookup (op =) insts ixn of
   56.49 -                  SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
   56.50 -                | _ => ixns union ixns'))
   56.51 +                  SOME (SOME t) => if is_proj t then union (op =) (ixns, ixns') else ixns'
   56.52 +                | _ => union (op =) (ixns, ixns')))
   56.53                    (needed prop ts'' prfs, add_npvars false true [] ([], prop));
   56.54              val insts' = map
   56.55                (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
   56.56                  | (_, x) => (false, x)) insts
   56.57            in ([], false, insts' @ map (pair false) ts'', prf) end
   56.58      and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
   56.59 -          (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
   56.60 +          union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
   56.61        | needed (Var (ixn, _)) (_::_) _ = [ixn]
   56.62        | needed _ _ _ = [];
   56.63    in shrink end;
    57.1 --- a/src/Pure/sorts.ML	Wed Oct 21 16:41:22 2009 +1100
    57.2 +++ b/src/Pure/sorts.ML	Wed Oct 21 08:16:25 2009 +0200
    57.3 @@ -72,8 +72,8 @@
    57.4  (** ordered lists of sorts **)
    57.5  
    57.6  val make = OrdList.make TermOrd.sort_ord;
    57.7 -val op subset = OrdList.subset TermOrd.sort_ord;
    57.8 -val op union = OrdList.union TermOrd.sort_ord;
    57.9 +val subset = OrdList.subset TermOrd.sort_ord;
   57.10 +val union = OrdList.union TermOrd.sort_ord;
   57.11  val subtract = OrdList.subtract TermOrd.sort_ord;
   57.12  
   57.13  val remove_sort = OrdList.remove TermOrd.sort_ord;
    58.1 --- a/src/Pure/thm.ML	Wed Oct 21 16:41:22 2009 +1100
    58.2 +++ b/src/Pure/thm.ML	Wed Oct 21 08:16:25 2009 +0200
    58.3 @@ -1463,7 +1463,7 @@
    58.4      (case duplicates (op =) cs of
    58.5        a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
    58.6      | [] =>
    58.7 -      (case cs inter_string freenames of
    58.8 +      (case inter (op =) (cs, freenames) of
    58.9          a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
   58.10        | [] =>
   58.11          Thm (der,
    59.1 --- a/src/Pure/variable.ML	Wed Oct 21 16:41:22 2009 +1100
    59.2 +++ b/src/Pure/variable.ML	Wed Oct 21 08:16:25 2009 +0200
    59.3 @@ -301,7 +301,7 @@
    59.4      val names = names_of ctxt;
    59.5      val (xs', names') =
    59.6        if is_body ctxt then Name.variants xs names |>> map Name.skolem
    59.7 -      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs);
    59.8 +      else (no_dups (inter (op =) (xs, ys)); no_dups (inter (op =) (xs, zs));
    59.9          (xs, fold Name.declare xs names));
   59.10    in ctxt |> new_fixes names' xs xs' end;
   59.11  
    60.1 --- a/src/Sequents/prover.ML	Wed Oct 21 16:41:22 2009 +1100
    60.2 +++ b/src/Sequents/prover.ML	Wed Oct 21 08:16:25 2009 +0200
    60.3 @@ -31,14 +31,14 @@
    60.4         dups);
    60.5  
    60.6  fun (Pack(safes,unsafes)) add_safes ths   = 
    60.7 -    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes))
    60.8 +    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,safes))
    60.9          val ths' = subtract Thm.eq_thm_prop dups ths
   60.10      in
   60.11          Pack(sort (make_ord less) (ths'@safes), unsafes)
   60.12      end;
   60.13  
   60.14  fun (Pack(safes,unsafes)) add_unsafes ths = 
   60.15 -    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes))
   60.16 +    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,unsafes))
   60.17          val ths' = subtract Thm.eq_thm_prop dups ths
   60.18      in
   60.19          Pack(safes, sort (make_ord less) (ths'@unsafes))
    61.1 --- a/src/Tools/Code/code_ml.ML	Wed Oct 21 16:41:22 2009 +1100
    61.2 +++ b/src/Tools/Code/code_ml.ML	Wed Oct 21 08:16:25 2009 +0200
    61.3 @@ -1028,7 +1028,7 @@
    61.4      val tyco = Sign.intern_type thy raw_tyco;
    61.5      val constrs = map (Code.check_const thy) raw_constrs;
    61.6      val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
    61.7 -    val _ = if gen_eq_set (op =) (constrs, constrs') then ()
    61.8 +    val _ = if eq_set (op =) (constrs, constrs') then ()
    61.9        else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
   61.10      val is_first = is_first_occ background;
   61.11      val background' = register_datatype tyco constrs background;
    62.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Oct 21 16:41:22 2009 +1100
    62.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Oct 21 08:16:25 2009 +0200
    62.3 @@ -139,13 +139,13 @@
    62.4        val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
    62.5        val (conds_tyvs,cond_vs) = 
    62.6            Library.foldl (fn ((tyvs, vs), t) => 
    62.7 -                    (Library.union
    62.8 +                    (union (op =)
    62.9                         (OldTerm.term_tvars t, tyvs),
   62.10 -                     Library.union 
   62.11 +                     union (op =)
   62.12                         (map Term.dest_Var (OldTerm.term_vars t), vs))) 
   62.13                  (([],[]), rule_conds);
   62.14        val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
   62.15 -      val vars_to_fix = Library.union (termvars, cond_vs);
   62.16 +      val vars_to_fix = union (op =) (termvars, cond_vs);
   62.17        val (renamings, names2) = 
   62.18            List.foldr (fn (((n,i),ty), (vs, names')) => 
   62.19                      let val n' = Name.variant names' n in
    63.1 --- a/src/Tools/Metis/metis_env.ML	Wed Oct 21 16:41:22 2009 +1100
    63.2 +++ b/src/Tools/Metis/metis_env.ML	Wed Oct 21 08:16:25 2009 +0200
    63.3 @@ -1,5 +1,5 @@
    63.4  (* Metis-specific ML environment *)
    63.5 -nonfix ++ -- RL mem union subset;
    63.6 +nonfix ++ -- RL mem;
    63.7  val explode = String.explode;
    63.8  val implode = String.implode;
    63.9  val print = TextIO.print;
    64.1 --- a/src/Tools/intuitionistic.ML	Wed Oct 21 16:41:22 2009 +1100
    64.2 +++ b/src/Tools/intuitionistic.ML	Wed Oct 21 08:16:25 2009 +0200
    64.3 @@ -50,7 +50,7 @@
    64.4      if member (fn ((ps1, c1), (ps2, c2)) =>
    64.5          c1 aconv c2 andalso
    64.6          length ps1 = length ps2 andalso
    64.7 -        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    64.8 +        eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    64.9      else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
   64.10    end);
   64.11  
    65.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Oct 21 16:41:22 2009 +1100
    65.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Oct 21 08:16:25 2009 +0200
    65.3 @@ -65,7 +65,7 @@
    65.4    in
    65.5      if has_duplicates (op =) lfrees then
    65.6        raise RecError "repeated variable name in pattern"
    65.7 -    else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
    65.8 +    else if not (subset (op =) (Term.add_frees rhs [], lfrees)) then
    65.9        raise RecError "extra variables on rhs"
   65.10      else if length middle > 1 then
   65.11        raise RecError "more than one non-variable in pattern"