# HG changeset patch
# User haftmann
# Date 1256105785 -7200
# Node ID 5018f6a76b3fbd83b98de6086405182564804707
# Parent  c61fe520602bdf868062fce16546d77d403411ae# Parent  8f9594c31de4b68aa843888fecacb8909712725d
merged

diff -r c61fe520602b -r 5018f6a76b3f NEWS
--- a/NEWS	Wed Oct 21 16:41:22 2009 +1100
+++ b/NEWS	Wed Oct 21 08:16:25 2009 +0200
@@ -213,6 +213,9 @@
 
 *** ML ***
 
+* Removed some old-style infix operations using polymorphic equality.
+INCOMPATIBILITY.
+
 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
 provides a high-level programming interface to synchronized state
 variables with atomic update.  This works via pure function
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Import/hol4rews.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -165,7 +165,7 @@
   val empty = []
   val copy = I
   val extend = I
-  fun merge _ = Library.gen_union Thm.eq_thm
+  fun merge _ = Library.union Thm.eq_thm
 )
 
 val hol4_debug = Unsynchronized.ref false
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -281,9 +281,10 @@
           | itr (a::rst) = i=a orelse itr rst
     in itr L end;
 
+infix union;
 fun [] union S = S
   | S union [] = S
-  | (a::rst) union S2 = rst union (insert (op =) a S2)
+  | (a::rst) union S2 = rst union (insert (op =) a S2);
 
 fun implode_subst [] = []
   | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
@@ -1229,7 +1230,7 @@
           | add_consts (_, cs) = cs
         val t_consts = add_consts(t,[])
     in
-        fn th => eq_set(t_consts,add_consts(prop_of th,[]))
+        fn th => eq_set (op =) (t_consts, add_consts (prop_of th, []))
     end
 
 fun split_name str =
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Import/shuffler.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -78,7 +78,7 @@
   val empty = []
   val copy = I
   val extend = I
-  fun merge _ = Library.gen_union Thm.eq_thm
+  fun merge _ = Library.union Thm.eq_thm
 )
 
 fun print_shuffles thy =
@@ -563,7 +563,7 @@
         let
             val th_consts = add_consts(prop_of th,[])
         in
-            eq_set(t_consts,th_consts)
+            eq_set (op =) (t_consts, th_consts)
         end
     end
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -244,7 +244,7 @@
 
 fun monomial_lcm m1 m2 =
   fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
-          (gen_union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
+          (union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
 
 fun monomial_multidegree m =
  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
@@ -314,7 +314,7 @@
   FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
 
 fun poly_variables p =
-  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
+  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
 
 (* Order monomials for human presentation.                                   *)
 
@@ -1059,7 +1059,7 @@
 
 fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
 let
- val vars = fold_rev (curry (gen_union (op aconvc)) o poly_variables)
+ val vars = fold_rev (curry (union (op aconvc)) o poly_variables)
               (pol::eqs @ map fst leqs) []
  val monoid = if linf then
       (poly_const rat_1,RealArith.Rational_lt rat_1)::
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Library/normarith.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -286,7 +286,7 @@
    val dests = distinct (op aconvc) (map snd rawdests)
    val srcfuns = map vector_lincomb sources
    val destfuns = map vector_lincomb dests 
-   val vvs = fold_rev (curry (gen_union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
+   val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
    val n = length srcfuns
    val nvs = 1 upto n
    val srccombs = srcfuns ~~ nvs
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -568,7 +568,7 @@
   fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
   val one_tm = @{cterm "1::real"}
   fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
-     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
+     ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
        not(p(FuncUtil.Ctermfunc.apply e one_tm)))
 
   fun linear_ineqs vars (les,lts) = 
@@ -620,7 +620,7 @@
   | NONE => (case eqs of 
     [] => 
      let val vars = remove (op aconvc) one_tm 
-           (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
+           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
      in linear_ineqs vars (les,lts) end
    | (e,p)::es => 
      if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
@@ -679,7 +679,7 @@
   val le_pols = map rhs le
   val lt_pols = map rhs lt 
   val aliens =  filter is_alien
-      (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
+      (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
           (eq_pols @ le_pols @ lt_pols) [])
   val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -28,7 +28,7 @@
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
-fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
+fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
 
 val fresh_prod = thm "fresh_prod";
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -33,7 +33,7 @@
     [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
      @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
 
-fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
+fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
 
 val perm_bool = mk_meta_eq (thm "perm_bool");
 val perm_boolI = thm "perm_boolI";
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -228,7 +228,7 @@
       (case Symtab.lookup dt_info tname of
           NONE => primrec_err (quote tname ^ " is not a nominal datatype")
         | SOME dt =>
-            if tnames' subset (map (#1 o snd) (#descr dt)) then
+            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
@@ -251,7 +251,7 @@
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
       map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
     val _ =
-      (if forall (curry eq_set lsrs) lsrss andalso forall
+      (if forall (curry (eq_set (op =)) lsrs) lsrss andalso forall
          (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
                forall (fn (_, (ls', _, rs', _, _)) =>
                  ls = ls' andalso rs = rs') eqns
@@ -276,7 +276,7 @@
     val defs' = map (make_def lthy fixes fs) defs;
     val names1 = map snd fnames;
     val names2 = map fst eqns;
-    val _ = if gen_eq_set (op =) (names1, names2) then ()
+    val _ = if eq_set (op =) (names1, names2) then ()
       else primrec_err ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val (defs_thms, lthy') = lthy |>
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/SMT/Tools/smt_monomorph.ML
--- a/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -55,7 +55,7 @@
 fun proper_match ps env =
   forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
 
-val eq_tab = gen_eq_set (op =) o pairself Vartab.dest
+val eq_tab = eq_set (op =) o pairself Vartab.dest
 
 fun specialize thy cs is ((r, ps), ces) (ts, ns) =
   let
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Set.thy	Wed Oct 21 08:16:25 2009 +0200
@@ -303,7 +303,7 @@
       fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
         | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
             n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
-            ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
+            subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
         | check _ = false
 
         fun tr' (_ $ abs) =
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -124,7 +124,7 @@
       |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
     
     val tycos = map fst dataTs;
-    val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
+    val _ = if eq_set (op =) (tycos, raw_tycos) then ()
       else error ("Type constructors " ^ commas (map quote raw_tycos)
         ^ " do not belong exhaustively to one mutual recursive datatype");
 
@@ -489,7 +489,7 @@
     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
       let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
       in (case duplicates (op =) tvs of
-            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+            [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
                   else error ("Mutually recursive datatypes must have same type parameters")
           | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
               " : " ^ commas dups))
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -257,7 +257,7 @@
 fun get_nonrec_types descr sorts =
   map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
     Library.foldl (fn (Ts', (_, cargs)) =>
-      filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
+      union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
 
 (* get all recursive types in datatype description *)
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -90,7 +90,7 @@
       IntGraph.empty
         |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
         |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
-               if i = j orelse null (c1 inter t2) 
+               if i = j orelse null (inter (op =) (c1, t2))
                then I else IntGraph.add_edge_acyclic (i,j))
              num_branches num_branches
     end
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -101,7 +101,7 @@
           let
             val t = Pattern.rewrite_term thy sigma [] feq1
           in
-            fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
+            fold_rev Logic.all (inter (op =) (map Free (frees_in_term ctx t), vs')) t
           end
     in
       map instantiate substs
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -348,7 +348,7 @@
   | Add(lin1,lin2) =>
         let val lis1 = resolve_proof vars lin1
             val lis2 = resolve_proof vars lin2
-            val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
+            val dom = distinct (op =) (union (op =) (map fst lis1, map fst lis2))
         in
             map (fn n => let val a = these (AList.lookup (op =) lis1 n)
                              val b = these (AList.lookup (op =) lis2 n)
@@ -884,7 +884,7 @@
  fun isolate_monomials vars tm =
  let 
   val (cmons,vmons) =
-    List.partition (fn m => null (gen_inter op aconvc (frees m, vars)))
+    List.partition (fn m => null (inter op aconvc (frees m, vars)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -984,20 +984,20 @@
             val dupTs = map snd (duplicates (op =) vTs) @
               map_filter (AList.lookup (op =) vTs) vs;
           in
-            terms_vs (in_ts @ in_ts') subset vs andalso
+            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
             forall (is_eqT o fastype_of) in_ts' andalso
-            term_vs t subset vs andalso
+            subset (op =) (term_vs t, vs) andalso
             forall is_eqT dupTs
           end)
             (modes_of_term modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
       | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
             length us = length is andalso
-            terms_vs us subset vs andalso
-            term_vs t subset vs)
+            subset (op =) (terms_vs us, vs) andalso
+            subset (op =) (term_vs t, vs))
             (modes_of_term modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
-      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
           else NONE
       ) ps);
 
@@ -1047,16 +1047,16 @@
             (if with_generator then
               (case select_mode_prem thy gen_modes' vs ps of
                 SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
-                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+                  (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
                   (filter_out (equal p) ps)
               | _ =>
                   let 
                     val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
                   in
                     case (find_first (fn generator_vs => is_some
-                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
+                      (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
                       SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
-                        (vs union generator_vs) ps
+                        (union (op =) (vs, generator_vs)) ps
                     | NONE => let
                     val _ = tracing ("ps:" ^ (commas
                     (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
@@ -1065,7 +1065,7 @@
             else
               NONE)
         | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
-            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+            (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
             (filter_out (equal p) ps))
     val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
     val in_vs = terms_vs in_ts;
@@ -1073,13 +1073,13 @@
   in
     if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
     forall (is_eqT o fastype_of) in_ts' then
-      case check_mode_prems [] (param_vs union in_vs) ps of
+      case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
          NONE => NONE
        | SOME (acc_ps, vs) =>
          if with_generator then
            SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
          else
-           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
+           if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
     else NONE
   end;
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -308,7 +308,7 @@
   | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   | _ => (acc, dacc)
   val (cs,ds) = h ([],[]) p
-  val l = Integer.lcms (cs union ds)
+  val l = Integer.lcms (union (op =) (cs, ds))
   fun cv k ct =
     let val (tm as b$s$t) = term_of ct
     in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -84,7 +84,7 @@
  in h [] end;
 in 
 fun is_relevant ctxt ct = 
- gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
+ subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
  andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
  andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/TFL/post.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -28,7 +28,7 @@
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
     map (Type.freeze o HOLogic.dest_Trueprop)
-      (List.foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
+      (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------
  * Three postprocessors are applied to the definition.  It
@@ -79,7 +79,7 @@
       val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
       val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
       val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
-      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
+      val cntxt = union (op aconv) (cntxtl, cntxtr)
   in
     R.GEN_ALL
       (R.DISCH_ALL
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -531,7 +531,7 @@
                  then writeln (cat_lines ("Extractants =" ::
                   map (Display.string_of_thm_global thy) extractants))
                  else ()
-     val TCs = List.foldr (gen_union (op aconv)) [] TCl
+     val TCs = List.foldr (union (op aconv)) [] TCl
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -202,15 +202,15 @@
             val dupTs = map snd (duplicates (op =) vTs) @
               map_filter (AList.lookup (op =) vTs) vs;
           in
-            terms_vs (in_ts @ in_ts') subset vs andalso
+            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
             forall (is_eqT o fastype_of) in_ts' andalso
-            term_vs t subset vs andalso
+            subset (op =) (term_vs t, vs) andalso
             forall is_eqT dupTs
           end)
             (if is_set then [Mode (([], []), [], [])]
              else modes_of modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
-      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
           else NONE) ps);
 
 fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
@@ -222,7 +222,7 @@
       | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
           NONE => NONE
         | SOME (x, _) => check_mode_prems
-            (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
+            (case x of Prem (us, _, _) => union (op =) (vs, terms_vs us) | _ => vs)
             (filter_out (equal x) ps));
     val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
     val in_vs = terms_vs in_ts;
@@ -230,9 +230,9 @@
   in
     forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
     forall (is_eqT o fastype_of) in_ts' andalso
-    (case check_mode_prems (arg_vs union in_vs) ps of
+    (case check_mode_prems (union (op =) (arg_vs, in_vs)) ps of
        NONE => false
-     | SOME vs => concl_vs subset vs)
+     | SOME vs => subset (op =) (concl_vs, vs))
   end;
 
 fun check_modes_pred thy arg_vs preds modes (p, ms) =
@@ -482,7 +482,7 @@
 fun constrain cs [] = []
   | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
       NONE => xs
-    | SOME xs' => xs inter xs') :: constrain cs ys;
+    | SOME xs' => inter (op =) (xs, xs')) :: constrain cs ys;
 
 fun mk_extra_defs thy defs gr dep names module ts =
   Library.foldl (fn (gr, name) =>
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -209,7 +209,7 @@
       (case optf of
          NONE => fs
        | SOME f => AList.update op = (u, the_default f
-           (Option.map (curry op inter f) (AList.lookup op = fs u))) fs));
+           (Option.map (curry (inter (op =)) f) (AList.lookup op = fs u))) fs));
 
 
 (**************************************************************)
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -631,7 +631,7 @@
         let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
         in
            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
-            tfrees = tfree_lits union tfrees}
+            tfrees = union (op =) (tfree_lits, tfrees)}
         end;
       val lmap0 = List.foldl (add_thm true)
                         {axioms = [], tfrees = init_tfrees ctxt} cls
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/old_primrec.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -226,7 +226,7 @@
       (case Symtab.lookup dt_info tname of
           NONE => primrec_err (quote tname ^ " is not a datatype")
         | SOME dt =>
-            if tnames' subset (map (#1 o snd) (#descr dt)) then
+            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
@@ -265,7 +265,7 @@
     val defs' = map (make_def thy fs) defs;
     val nameTs1 = map snd fnameTs;
     val nameTs2 = map fst rec_eqns;
-    val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
+    val _ = if eq_set (op =) (nameTs1, nameTs2) then ()
             else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
               "\nare not mutually recursive");
     val primrec_name =
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/primrec.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -208,7 +208,7 @@
       (case Symtab.lookup dt_info tname of
           NONE => primrec_error (quote tname ^ " is not a datatype")
         | SOME dt =>
-            if tnames' subset (map (#1 o snd) (#descr dt)) then
+            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
@@ -232,7 +232,7 @@
     val defs = map (make_def lthy fixes fs) raw_defs;
     val names = map snd fnames;
     val names_eqns = map fst eqns;
-    val _ = if gen_eq_set (op =) (names, names_eqns) then ()
+    val _ = if eq_set (op =) (names, names_eqns) then ()
       else primrec_error ("functions " ^ commas_quote names_eqns ^
         "\nare not mutually recursive");
     val rec_rewrites' = map mk_meta_eq rec_rewrites;
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/prop_logic.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -111,8 +111,8 @@
 	  | indices False            = []
 	  | indices (BoolVar i)      = [i]
 	  | indices (Not fm)         = indices fm
-	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
-	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
+	  | indices (Or (fm1, fm2))  = union (op =) (indices fm1, indices fm2)
+	  | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2);
 
 (* ------------------------------------------------------------------------- *)
 (* maxidx: computes the maximal variable index occuring in a formula of      *)
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/record.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -1834,7 +1834,7 @@
     val extN = full bname;
     val types = map snd fields;
     val alphas_fields = fold Term.add_tfree_namesT types [];
-    val alphas_ext = alphas inter alphas_fields;
+    val alphas_ext = inter (op =) (alphas, alphas_fields);
     val len = length fields;
     val variants =
       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/refute.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -1154,7 +1154,7 @@
       val axioms = collect_axioms thy u
       (* Term.typ list *)
       val types = Library.foldl (fn (acc, t') =>
-        acc union (ground_types thy t')) ([], u :: axioms)
+        union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
       val _     = tracing ("Ground types: "
         ^ (if null types then "none."
            else commas (map (Syntax.string_of_typ_global thy) types)))
@@ -2415,7 +2415,7 @@
                       (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
                   (* sanity check: typ_assoc must associate types to the   *)
                   (*               elements of 'dtyps' (and only to those) *)
-                  val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
+                  val _ = if not (eq_set (op =) (dtyps, map fst typ_assoc))
                     then
                       raise REFUTE ("IDT_recursion_interpreter",
                         "type association has extra/missing elements")
@@ -3007,7 +3007,7 @@
         [Type ("fun", [T, Type ("bool", [])]),
          Type ("fun", [_, Type ("bool", [])])]),
          Type ("fun", [_, Type ("bool", [])])])) =>
-      let nonfix union (* because "union" is used below *)
+      let
         val size_elem = size_of_type thy model T
         (* the universe (i.e. the set that contains every element) *)
         val i_univ = Node (replicate size_elem TT)
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/res_atp.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -211,8 +211,9 @@
         fun defs lhs rhs =
             let val (rator,args) = strip_comb lhs
                 val ct = const_with_typ thy (dest_ConstFree rator)
-            in  forall is_Var args andalso uni_mem gctypes ct andalso
-                Term.add_vars rhs [] subset Term.add_vars lhs []
+            in
+              forall is_Var args andalso uni_mem gctypes ct andalso
+                subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
             end
             handle ConstFree => false
     in    
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -473,7 +473,7 @@
       val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
                                       (map Thm.term_of hyps)
       val fixed = OldTerm.term_frees (concl_of st) @
-                  List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
+                  List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
   in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
 
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/res_clause.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -93,7 +93,7 @@
 val tconst_prefix = "tc_";
 val class_prefix = "class_";
 
-fun union_all xss = List.foldl (op union) [] xss;
+fun union_all xss = List.foldl (union (op =)) [] xss;
 
 (*Provide readable names for the more common symbolic functions*)
 val const_trans_table =
@@ -263,7 +263,7 @@
   | pred_of_sort (LTFree (s,ty)) = (s,1)
 
 (*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts);
+fun add_typs Ts = List.foldl (union (op =)) [] (map sorts_on_typs Ts);
 
 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
@@ -372,7 +372,7 @@
       let val cpairs = type_class_pairs thy tycons classes
           val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
-      in  (classes' union classes, cpairs' union cpairs)  end;
+      in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;
 
 fun make_arity_clauses_dfg dfg thy tycons classes =
   let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -155,7 +155,7 @@
   | combterm_of dfg thy (P $ Q) =
       let val (P',tsP) = combterm_of dfg thy P
           val (Q',tsQ) = combterm_of dfg thy Q
-      in  (CombApp(P',Q'), tsP union tsQ)  end
+      in  (CombApp(P',Q'), union (op =) (tsP, tsQ))  end
   | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
 
 fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
@@ -167,7 +167,7 @@
   | literals_of_term1 dfg thy (lits,ts) P =
       let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
       in
-          (Literal(pol,pred)::lits, ts union ts')
+          (Literal(pol,pred)::lits, union (op =) (ts, ts'))
       end;
 
 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
@@ -476,7 +476,7 @@
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
-    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
+    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (union (op =)) [] tfree_litss)
     val _ =
       File.write_list file (
         map (#1 o (clause2tptp params)) axclauses @
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -364,7 +364,7 @@
 fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
 
 fun replace_deps (old:int, new) (lno, t, deps) =
-      (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps));
+      (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps));
 
 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   only in type information.*)
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -471,8 +471,8 @@
         | forced_vars False             = []
         | forced_vars (BoolVar i)       = [i]
         | forced_vars (Not (BoolVar i)) = [~i]
-        | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
-        | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
+        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1, forced_vars fm2)
+        | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1, forced_vars fm2)
         (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
         (* precedence, and the next partial evaluation of the formula returns 'False'. *)
         | forced_vars _                 = error "formula is not in negation normal form"
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/transfer.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -143,7 +143,7 @@
  {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
   ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
   hints = subtract (op = : string*string -> bool) hints0
-            (hints1 union_string hints2)}
+            (union (op =) (hints1, hints2))}
  end;
 
 local
@@ -151,7 +151,7 @@
 in
 fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
                    {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
-    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
+    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = union (op =) (hints1, hints2)}
 end;
 
 fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
diff -r c61fe520602b -r 5018f6a76b3f src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/ex/predicate_compile.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -908,20 +908,20 @@
             val dupTs = map snd (duplicates (op =) vTs) @
               map_filter (AList.lookup (op =) vTs) vs;
           in
-            terms_vs (in_ts @ in_ts') subset vs andalso
+            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
             forall (is_eqT o fastype_of) in_ts' andalso
-            term_vs t subset vs andalso
+            subset (op =) (term_vs t, vs) andalso
             forall is_eqT dupTs
           end)
             (modes_of_term modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
       | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
             length us = length is andalso
-            terms_vs us subset vs andalso
-            term_vs t subset vs)
+            subset (op =) (terms_vs us, vs) andalso
+            subset (op =) (term_vs t, vs)
             (modes_of_term modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
-      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
           else NONE
       ) ps);
 
@@ -964,22 +964,22 @@
             (if with_generator then
               (case select_mode_prem thy gen_modes' vs ps of
                   SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
-                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+                  (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
                   (filter_out (equal p) ps)
                 | NONE =>
                   let 
                     val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
                   in
                     case (find_first (fn generator_vs => is_some
-                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
+                      (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
                       SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
-                        (vs union generator_vs) ps
+                        (union (op =) (vs, generator_vs)) ps
                     | NONE => NONE
                   end)
             else
               NONE)
         | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
-            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+            (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
             (filter_out (equal p) ps))
     val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
     val in_vs = terms_vs in_ts;
@@ -987,13 +987,13 @@
   in
     if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
     forall (is_eqT o fastype_of) in_ts' then
-      case check_mode_prems [] (param_vs union in_vs) ps of
+      case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
          NONE => NONE
        | SOME (acc_ps, vs) =>
          if with_generator then
            SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
          else
-           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
+           if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
     else NONE
   end;
 
diff -r c61fe520602b -r 5018f6a76b3f src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -59,8 +59,8 @@
             fun analyse indirect (TFree(v,s))  =
                 (case AList.lookup (op =) tvars v of 
                    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
-                 | SOME sort => if eq_set_string (s,defaultS) orelse
-                                   eq_set_string (s,sort    )
+                 | SOME sort => if eq_set (op =) (s, defaultS) orelse
+                                   eq_set (op =) (s, sort)
                                 then TFree(v,sort)
                                 else error ("Inconsistent sort constraint" ^
                                             " for type variable " ^ quote v))
diff -r c61fe520602b -r 5018f6a76b3f src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -74,7 +74,7 @@
 fun proc ss t =
   let val (divs,mods) = coll_div_mod t ([],[])
   in if null divs orelse null mods then NONE
-     else case divs inter mods of
+     else case inter (op =) (divs, mods) of
             pq :: _ => SOME (cancel ss t pq)
           | [] => NONE
   end
diff -r c61fe520602b -r 5018f6a76b3f src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -385,7 +385,7 @@
   let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
   if not (null eqs) then
      let val c =
-           fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs []
+           fold (fn Lineq(_,_,l,_) => fn cs => union (op =) (l, cs)) eqs []
            |> filter (fn i => i <> 0)
            |> sort (int_ord o pairself abs)
            |> hd
@@ -429,8 +429,8 @@
 val warning_count = Unsynchronized.ref 0;
 val warning_count_max = 10;
 
-val union_term = curry (gen_union Pattern.aeconv);
-val union_bterm = curry (gen_union
+val union_term = curry (union Pattern.aeconv);
+val union_bterm = curry (union
   (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
 
 fun add_atoms (lhs, _, _, rhs, _, _) =
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/General/name_space.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -145,7 +145,7 @@
       space
       |> add_name' name name
       |> fold (del_name name)
-        (if fully then names else names inter_string [Long_Name.base_name name])
+        (if fully then names else inter (op =) (names, [Long_Name.base_name name]))
       |> fold (del_name_extra name) (get_accesses space name)
     end;
 
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/General/ord_list.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -56,7 +56,6 @@
 
 (* lists as sets *)
 
-nonfix subset;
 fun subset ord (list1, list2) =
   let
     fun sub [] _ = true
@@ -75,7 +74,6 @@
 fun handle_same f x = f x handle SAME => x;
 
 (*union: insert elements of first list into second list*)
-nonfix union;
 fun union ord list1 list2 =
   let
     fun unio [] _ = raise SAME
@@ -88,7 +86,6 @@
   in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
 
 (*intersection: filter second list for elements present in first list*)
-nonfix inter;
 fun inter ord list1 list2 =
   let
     fun intr _ [] = raise SAME
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/General/path.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -42,7 +42,7 @@
   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
   | check_elem chs =
-      (case ["/", "\\", "$", ":"] inter_string chs of
+      (case inter (op =) (["/", "\\", "$", ":"], chs) of
         [] => chs
       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
 
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Proof/extraction.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -198,7 +198,7 @@
     {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
      typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
      types = AList.merge (op =) (K true) (types1, types2),
-     realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
+     realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
      defs = Library.merge Thm.eq_thm (defs1, defs2),
      expand = Library.merge (op =) (expand1, expand2),
      prep = (case prep1 of NONE => prep2 | _ => prep1)};
@@ -468,7 +468,7 @@
 
       in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
 
-    fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
+    fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
     fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
 
     fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Proof/reconstruct.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -289,7 +289,7 @@
     val _ = message "Collecting constraints...";
     val (t, prf, cs, env, _) = make_constraints_cprf thy
       (Envir.empty (maxidx_proof cprf ~1)) cprf';
-    val cs' = map (fn p => (true, p, op union
+    val cs' = map (fn p => (true, p, union (op =) 
         (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
       (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
     val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -77,7 +77,7 @@
   |> command K.prf_asm_goal     goal
   |> command K.prf_script       proofstep;
 
-val _ = OuterKeyword.kinds subset_string Symtab.keys command_keywords
+val _ = subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
   orelse sys_error "Incomplete coverage of command keywords";
 
 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Syntax/ast.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -104,7 +104,7 @@
     val rvars = add_vars rhs [];
   in
     if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
-    else if not (rvars subset lvars) then SOME "rhs contains extra variables"
+    else if not (subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
     else NONE
   end;
 
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Syntax/parser.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -101,7 +101,7 @@
 
             val tos = connected_with chains' [lhs] [lhs];
         in (copy_lookahead tos [],
-            gen_union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
+            union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
         end;
 
       (*test if new production can produce lambda
@@ -109,7 +109,7 @@
       val (new_lambda, lambdas') =
         if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
                     | (Terminal _) => false) rhs then
-          (true, gen_union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
+          (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
         else
           (false, lambdas');
 
@@ -125,7 +125,7 @@
       (*get all known starting tokens for a nonterminal*)
       fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
 
-      val token_union = gen_union matching_tokens;
+      val token_union = union matching_tokens;
 
       (*update prods, lookaheads, and lambdas according to new lambda NTs*)
       val (added_starts', lambdas') =
@@ -147,7 +147,7 @@
                     in
                       if member (op =) nts l then       (*update production's lookahead*)
                       let
-                        val new_lambda = is_none tk andalso nts subset lambdas;
+                        val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
 
                         val new_tks = subtract (op =) l_starts
                           ((if is_some tk then [the tk] else []) @
@@ -155,7 +155,7 @@
 
                         val added_tks' = token_union (new_tks, added_tks);
 
-                        val nt_dependencies' = gen_union (op =) (nts, nt_dependencies);
+                        val nt_dependencies' = union (op =) (nts, nt_dependencies);
 
                         (*associate production with new starting tokens*)
                         fun copy ([]: token option list) nt_prods = nt_prods
@@ -413,7 +413,7 @@
         fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
 
         val nt_prods =
-          Library.foldl (gen_union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
+          Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
           map prod_of_chain ((these o AList.lookup (op =) chains) tag);
       in map (pretty_prod name) nt_prods end;
 
@@ -562,7 +562,7 @@
     fun process_nt ~1 result = result
       | process_nt nt result =
         let
-          val nt_prods = Library.foldl (gen_union op =)
+          val nt_prods = Library.foldl (union op =)
                              ([], map snd (snd (Array.sub (prods2, nt))));
           val lhs_tag = convert_tag nt;
 
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -352,7 +352,7 @@
   in
     SynExt {
       xprods = xprods,
-      consts = consts union_string mfix_consts,
+      consts = union (op =) (consts, mfix_consts),
       prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
       parse_ast_translation = parse_ast_translation,
       parse_rules = parse_rules' @ parse_rules,
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -248,7 +248,7 @@
 
     fun check (t, NONE) = check (t, SOME (get_thm_names t))
       | check ((_, thm), c as SOME thm_consts) =
-         (if pat_consts subset_string thm_consts andalso
+         (if subset (op =) (pat_consts, thm_consts) andalso
             Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
           then SOME (0, 0) else NONE, c);
   in check end;
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/codegen.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -599,8 +599,8 @@
      else Pretty.block (separate (Pretty.brk 1) (p :: ps));
 
 fun new_names t xs = Name.variant_list
-  (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
-    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
+  (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
+    OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
 
 fun new_name t x = hd (new_names t [x]);
 
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/library.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -11,8 +11,7 @@
 infix 2 ?
 infix 3 o oo ooo oooo
 infix 4 ~~ upto downto
-infix orf andf \ \\ mem mem_int mem_string union union_int
-  union_string inter inter_int inter_string subset subset_int subset_string
+infix orf andf \ \\ mem mem_int mem_string
 
 signature BASIC_LIBRARY =
 sig
@@ -163,21 +162,10 @@
   val mem: ''a * ''a list -> bool
   val mem_int: int * int list -> bool
   val mem_string: string * string list -> bool
-  val union: ''a list * ''a list -> ''a list
-  val union_int: int list * int list -> int list
-  val union_string: string list * string list -> string list
-  val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
-  val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
-  val inter: ''a list * ''a list -> ''a list
-  val inter_int: int list * int list -> int list
-  val inter_string: string list * string list -> string list
-  val subset: ''a list * ''a list -> bool
-  val subset_int: int list * int list -> bool
-  val subset_string: string list * string list -> bool
-  val eq_set: ''a list * ''a list -> bool
-  val eq_set_string: string list * string list -> bool
-  val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
-  val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
+  val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
+  val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val \ : ''a list * ''a -> ''a list
   val \\ : ''a list * ''a list -> ''a list
   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
@@ -811,73 +799,23 @@
 fun (x: string) mem_string xs = member (op =) xs x;
 
 (*union of sets represented as lists: no repetitions*)
-fun xs union [] = xs
-  | [] union ys = ys
-  | (x :: xs) union ys = xs union (insert (op =) x ys);
-
-(*union of sets, optimized version for ints*)
-fun (xs:int list) union_int [] = xs
-  | [] union_int ys = ys
-  | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
-
-(*union of sets, optimized version for strings*)
-fun (xs:string list) union_string [] = xs
-  | [] union_string ys = ys
-  | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
-
-(*generalized union*)
-fun gen_union eq (xs, []) = xs
-  | gen_union eq ([], ys) = ys
-  | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
-
+fun union eq (xs, []) = xs
+  | union eq ([], ys) = ys
+  | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
 
 (*intersection*)
-fun [] inter ys = []
-  | (x :: xs) inter ys =
-      if x mem ys then x :: (xs inter ys) else xs inter ys;
-
-(*intersection, optimized version for ints*)
-fun ([]:int list) inter_int ys = []
-  | (x :: xs) inter_int ys =
-      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
-
-(*intersection, optimized version for strings *)
-fun ([]:string list) inter_string ys = []
-  | (x :: xs) inter_string ys =
-      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
-
-(*generalized intersection*)
-fun gen_inter eq ([], ys) = []
-  | gen_inter eq (x::xs, ys) =
-      if member eq ys x then x :: gen_inter eq (xs, ys)
-      else gen_inter eq (xs, ys);
-
+fun inter eq ([], ys) = []
+  | inter eq (x::xs, ys) =
+      if member eq ys x then x :: inter eq (xs, ys)
+      else inter eq (xs, ys);
 
 (*subset*)
-fun [] subset ys = true
-  | (x :: xs) subset ys = x mem ys andalso xs subset ys;
-
-(*subset, optimized version for ints*)
-fun ([]: int list) subset_int ys = true
-  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
-
-(*subset, optimized version for strings*)
-fun ([]: string list) subset_string ys = true
-  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
+fun subset eq (xs, ys) = forall (member eq ys) xs;
 
 (*set equality*)
-fun eq_set (xs, ys) =
-  xs = ys orelse (xs subset ys andalso ys subset xs);
-
-(*set equality for strings*)
-fun eq_set_string ((xs: string list), ys) =
-  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
-
-fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
-
-fun gen_eq_set eq (xs, ys) =
+fun eq_set eq (xs, ys) =
   eq_list eq (xs, ys) orelse
-    (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
+    (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
 
 
 (*removing an element from a list WITHOUT duplicates*)
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/meta_simplifier.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -398,7 +398,7 @@
   | vperm (t, u) = (t = u);
 
 fun var_perm (t, u) =
-  vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
+  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
 
 (*simple test for looping rewrite rules and stupid orientations*)
 fun default_reorient thy prems lhs rhs =
@@ -864,7 +864,7 @@
   while the premises are solved.*)
 
 fun cond_skel (args as (_, (lhs, rhs))) =
-  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
+  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
   else skel0;
 
 (*
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/pattern.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -216,10 +216,10 @@
 
 fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
-            if js subset_int is
+            if subset (op =) (js, is)
             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
                  in Envir.update (((F, Fty), t), env) end
-            else let val ks = is inter_int js
+            else let val ks = inter (op =) (is, js)
                      val Hty = type_of_G env (Fty,length is,map (idx is) ks)
                      val (env',H) = Envir.genvar a (env,Hty)
                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
@@ -339,7 +339,7 @@
   let val js = loose_bnos t
   in if null is
      then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
-     else if js subset_int is
+     else if subset (op =) (js, is)
           then let val t' = if downto0(is,length binders - 1) then t
                             else mapbnd (idx is) t
                in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/proofterm.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -900,8 +900,8 @@
 
 fun add_funvars Ts (vs, t) =
   if is_fun (fastype_of1 (Ts, t)) then
-    vs union map_filter (fn Var (ixn, T) =>
-      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)
+    union (op =) (vs, map_filter (fn Var (ixn, T) =>
+      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
   else vs;
 
 fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
@@ -918,7 +918,7 @@
   | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
 
-fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
+fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P, prop_vars Q)
   | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
   | prop_vars t = (case strip_comb t of
       (Var (ixn, _), _) => [ixn] | _ => []);
@@ -936,9 +936,9 @@
   end;
 
 fun needed_vars prop =
-  Library.foldl (op union)
-    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
-  prop_vars prop;
+  union (op =) (Library.foldl (union (op =))
+    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
+  prop_vars prop);
 
 fun gen_axm_proof c name prop =
   let
@@ -975,7 +975,7 @@
           let
             val p as (_, is', ch', prf') = shrink ls lev prf2;
             val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
-          in (is union is', ch orelse ch', ts',
+          in (union (op =) (is, is'), ch orelse ch', ts',
               if ch orelse ch' then prf'' %% prf' else prf)
           end
       | shrink' ls lev ts prfs (prf as prf1 % t) =
@@ -1004,15 +1004,15 @@
             val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
               insert (op =) ixn (case AList.lookup (op =) insts ixn of
-                  SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
-                | _ => ixns union ixns'))
+                  SOME (SOME t) => if is_proj t then union (op =) (ixns, ixns') else ixns'
+                | _ => union (op =) (ixns, ixns')))
                   (needed prop ts'' prfs, add_npvars false true [] ([], prop));
             val insts' = map
               (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
                 | (_, x) => (false, x)) insts
           in ([], false, insts' @ map (pair false) ts'', prf) end
     and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
-          (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
+          union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
       | needed (Var (ixn, _)) (_::_) _ = [ixn]
       | needed _ _ _ = [];
   in shrink end;
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/sorts.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -72,8 +72,8 @@
 (** ordered lists of sorts **)
 
 val make = OrdList.make TermOrd.sort_ord;
-val op subset = OrdList.subset TermOrd.sort_ord;
-val op union = OrdList.union TermOrd.sort_ord;
+val subset = OrdList.subset TermOrd.sort_ord;
+val union = OrdList.union TermOrd.sort_ord;
 val subtract = OrdList.subtract TermOrd.sort_ord;
 
 val remove_sort = OrdList.remove TermOrd.sort_ord;
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/thm.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -1463,7 +1463,7 @@
     (case duplicates (op =) cs of
       a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
     | [] =>
-      (case cs inter_string freenames of
+      (case inter (op =) (cs, freenames) of
         a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
       | [] =>
         Thm (der,
diff -r c61fe520602b -r 5018f6a76b3f src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/variable.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -301,7 +301,7 @@
     val names = names_of ctxt;
     val (xs', names') =
       if is_body ctxt then Name.variants xs names |>> map Name.skolem
-      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs);
+      else (no_dups (inter (op =) (xs, ys)); no_dups (inter (op =) (xs, zs));
         (xs, fold Name.declare xs names));
   in ctxt |> new_fixes names' xs xs' end;
 
diff -r c61fe520602b -r 5018f6a76b3f src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Sequents/prover.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -31,14 +31,14 @@
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
-    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes))
+    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,safes))
         val ths' = subtract Thm.eq_thm_prop dups ths
     in
         Pack(sort (make_ord less) (ths'@safes), unsafes)
     end;
 
 fun (Pack(safes,unsafes)) add_unsafes ths = 
-    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes))
+    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,unsafes))
         val ths' = subtract Thm.eq_thm_prop dups ths
     in
         Pack(safes, sort (make_ord less) (ths'@unsafes))
diff -r c61fe520602b -r 5018f6a76b3f src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Tools/Code/code_ml.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -1028,7 +1028,7 @@
     val tyco = Sign.intern_type thy raw_tyco;
     val constrs = map (Code.check_const thy) raw_constrs;
     val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
-    val _ = if gen_eq_set (op =) (constrs, constrs') then ()
+    val _ = if eq_set (op =) (constrs, constrs') then ()
       else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
     val is_first = is_first_occ background;
     val background' = register_datatype tyco constrs background;
diff -r c61fe520602b -r 5018f6a76b3f src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -139,13 +139,13 @@
       val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
       val (conds_tyvs,cond_vs) = 
           Library.foldl (fn ((tyvs, vs), t) => 
-                    (Library.union
+                    (union (op =)
                        (OldTerm.term_tvars t, tyvs),
-                     Library.union 
+                     union (op =)
                        (map Term.dest_Var (OldTerm.term_vars t), vs))) 
                 (([],[]), rule_conds);
       val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
-      val vars_to_fix = Library.union (termvars, cond_vs);
+      val vars_to_fix = union (op =) (termvars, cond_vs);
       val (renamings, names2) = 
           List.foldr (fn (((n,i),ty), (vs, names')) => 
                     let val n' = Name.variant names' n in
diff -r c61fe520602b -r 5018f6a76b3f src/Tools/Metis/metis_env.ML
--- a/src/Tools/Metis/metis_env.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Tools/Metis/metis_env.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -1,5 +1,5 @@
 (* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
diff -r c61fe520602b -r 5018f6a76b3f src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Tools/intuitionistic.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -50,7 +50,7 @@
     if member (fn ((ps1, c1), (ps2, c2)) =>
         c1 aconv c2 andalso
         length ps1 = length ps2 andalso
-        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
+        eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
     else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
   end);
 
diff -r c61fe520602b -r 5018f6a76b3f src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/ZF/Tools/primrec_package.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -65,7 +65,7 @@
   in
     if has_duplicates (op =) lfrees then
       raise RecError "repeated variable name in pattern"
-    else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
+    else if not (subset (op =) (Term.add_frees rhs [], lfrees)) then
       raise RecError "extra variables on rhs"
     else if length middle > 1 then
       raise RecError "more than one non-variable in pattern"