replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
authorhaftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037b22e44496dc2
parent 33015 575bd6548df9
child 33038 8f9594c31de4
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
NEWS
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Set.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/pattern_split.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/primrec.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_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_solver.ML
src/HOL/Tools/transfer.ML
src/HOL/ex/predicate_compile.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/Provers/Arith/cancel_div_mod.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/name_space.ML
src/Pure/General/ord_list.ML
src/Pure/General/path.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Tools/find_theorems.ML
src/Pure/codegen.ML
src/Pure/library.ML
src/Pure/meta_simplifier.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/sorts.ML
src/Pure/thm.ML
src/Pure/variable.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/Metis/metis_env.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/NEWS	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/NEWS	Tue Oct 20 16:13:01 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/proof_kernel.ML	Tue Oct 20 13:37:56 2009 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Oct 20 16:13:01 2009 +0200
     2.3 @@ -281,9 +281,10 @@
     2.4            | itr (a::rst) = i=a orelse itr rst
     2.5      in itr L end;
     2.6  
     2.7 +infix union;
     2.8  fun [] union S = S
     2.9    | S union [] = S
    2.10 -  | (a::rst) union S2 = rst union (insert (op =) a S2)
    2.11 +  | (a::rst) union S2 = rst union (insert (op =) a S2);
    2.12  
    2.13  fun implode_subst [] = []
    2.14    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
    2.15 @@ -1229,7 +1230,7 @@
    2.16            | add_consts (_, cs) = cs
    2.17          val t_consts = add_consts(t,[])
    2.18      in
    2.19 -        fn th => eq_set(t_consts,add_consts(prop_of th,[]))
    2.20 +        fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
    2.21      end
    2.22  
    2.23  fun split_name str =
     3.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 20 13:37:56 2009 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 20 16:13:01 2009 +0200
     3.3 @@ -563,7 +563,7 @@
     3.4          let
     3.5              val th_consts = add_consts(prop_of th,[])
     3.6          in
     3.7 -            eq_set(t_consts,th_consts)
     3.8 +            gen_eq_set (op =) (t_consts, th_consts)
     3.9          end
    3.10      end
    3.11  
     4.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 20 13:37:56 2009 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 20 16:13:01 2009 +0200
     4.3 @@ -228,7 +228,7 @@
     4.4        (case Symtab.lookup dt_info tname of
     4.5            NONE => primrec_err (quote tname ^ " is not a nominal datatype")
     4.6          | SOME dt =>
     4.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
     4.8 +            if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
     4.9                (tname, dt)::(find_dts dt_info tnames' tnames)
    4.10              else find_dts dt_info tnames' tnames);
    4.11  
    4.12 @@ -251,7 +251,7 @@
    4.13      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
    4.14        map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
    4.15      val _ =
    4.16 -      (if forall (curry eq_set lsrs) lsrss andalso forall
    4.17 +      (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall
    4.18           (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
    4.19                 forall (fn (_, (ls', _, rs', _, _)) =>
    4.20                   ls = ls' andalso rs = rs') eqns
     5.1 --- a/src/HOL/Set.thy	Tue Oct 20 13:37:56 2009 +0200
     5.2 +++ b/src/HOL/Set.thy	Tue Oct 20 16:13:01 2009 +0200
     5.3 @@ -303,7 +303,7 @@
     5.4        fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
     5.5          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
     5.6              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
     5.7 -            ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
     5.8 +            gen_subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
     5.9          | check _ = false
    5.10  
    5.11          fun tr' (_ $ abs) =
     6.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 20 13:37:56 2009 +0200
     6.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 20 16:13:01 2009 +0200
     6.3 @@ -489,7 +489,7 @@
     6.4      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
     6.5        let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
     6.6        in (case duplicates (op =) tvs of
     6.7 -            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
     6.8 +            [] => if gen_eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
     6.9                    else error ("Mutually recursive datatypes must have same type parameters")
    6.10            | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
    6.11                " : " ^ commas dups))
     7.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 20 13:37:56 2009 +0200
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 20 16:13:01 2009 +0200
     7.3 @@ -257,7 +257,7 @@
     7.4  fun get_nonrec_types descr sorts =
     7.5    map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
     7.6      Library.foldl (fn (Ts', (_, cargs)) =>
     7.7 -      filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
     7.8 +      gen_union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
     7.9  
    7.10  (* get all recursive types in datatype description *)
    7.11  
     8.1 --- a/src/HOL/Tools/Function/context_tree.ML	Tue Oct 20 13:37:56 2009 +0200
     8.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Tue Oct 20 16:13:01 2009 +0200
     8.3 @@ -90,7 +90,7 @@
     8.4        IntGraph.empty
     8.5          |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
     8.6          |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
     8.7 -               if i = j orelse null (c1 inter t2) 
     8.8 +               if i = j orelse null (gen_inter (op =) (c1, t2))
     8.9                 then I else IntGraph.add_edge_acyclic (i,j))
    8.10               num_branches num_branches
    8.11      end
     9.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Tue Oct 20 13:37:56 2009 +0200
     9.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Tue Oct 20 16:13:01 2009 +0200
     9.3 @@ -101,7 +101,7 @@
     9.4            let
     9.5              val t = Pattern.rewrite_term thy sigma [] feq1
     9.6            in
     9.7 -            fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
     9.8 +            fold_rev Logic.all (gen_inter (op =) (map Free (frees_in_term ctx t), vs')) t
     9.9            end
    9.10      in
    9.11        map instantiate substs
    10.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Oct 20 13:37:56 2009 +0200
    10.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Oct 20 16:13:01 2009 +0200
    10.3 @@ -348,7 +348,7 @@
    10.4    | Add(lin1,lin2) =>
    10.5          let val lis1 = resolve_proof vars lin1
    10.6              val lis2 = resolve_proof vars lin2
    10.7 -            val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
    10.8 +            val dom = distinct (op =) (gen_union (op =) (map fst lis1, map fst lis2))
    10.9          in
   10.10              map (fn n => let val a = these (AList.lookup (op =) lis1 n)
   10.11                               val b = these (AList.lookup (op =) lis2 n)
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 13:37:56 2009 +0200
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 16:13:01 2009 +0200
    11.3 @@ -984,20 +984,20 @@
    11.4              val dupTs = map snd (duplicates (op =) vTs) @
    11.5                map_filter (AList.lookup (op =) vTs) vs;
    11.6            in
    11.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
    11.8 +            gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
    11.9              forall (is_eqT o fastype_of) in_ts' andalso
   11.10 -            term_vs t subset vs andalso
   11.11 +            gen_subset (op =) (term_vs t, vs) andalso
   11.12              forall is_eqT dupTs
   11.13            end)
   11.14              (modes_of_term modes t handle Option =>
   11.15                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   11.16        | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
   11.17              length us = length is andalso
   11.18 -            terms_vs us subset vs andalso
   11.19 -            term_vs t subset vs)
   11.20 +            gen_subset (op =) (terms_vs us, vs) andalso
   11.21 +            gen_subset (op =) (term_vs t, vs))
   11.22              (modes_of_term modes t handle Option =>
   11.23                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   11.24 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   11.25 +      | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
   11.26            else NONE
   11.27        ) ps);
   11.28  
   11.29 @@ -1047,16 +1047,16 @@
   11.30              (if with_generator then
   11.31                (case select_mode_prem thy gen_modes' vs ps of
   11.32                  SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
   11.33 -                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   11.34 +                  (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
   11.35                    (filter_out (equal p) ps)
   11.36                | _ =>
   11.37                    let 
   11.38                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
   11.39                    in
   11.40                      case (find_first (fn generator_vs => is_some
   11.41 -                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
   11.42 +                      (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
   11.43                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
   11.44 -                        (vs union generator_vs) ps
   11.45 +                        (gen_union (op =) (vs, generator_vs)) ps
   11.46                      | NONE => let
   11.47                      val _ = tracing ("ps:" ^ (commas
   11.48                      (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
   11.49 @@ -1065,7 +1065,7 @@
   11.50              else
   11.51                NONE)
   11.52          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
   11.53 -            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   11.54 +            (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
   11.55              (filter_out (equal p) ps))
   11.56      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
   11.57      val in_vs = terms_vs in_ts;
   11.58 @@ -1073,13 +1073,13 @@
   11.59    in
   11.60      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   11.61      forall (is_eqT o fastype_of) in_ts' then
   11.62 -      case check_mode_prems [] (param_vs union in_vs) ps of
   11.63 +      case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
   11.64           NONE => NONE
   11.65         | SOME (acc_ps, vs) =>
   11.66           if with_generator then
   11.67             SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
   11.68           else
   11.69 -           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
   11.70 +           if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
   11.71      else NONE
   11.72    end;
   11.73  
    12.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 20 13:37:56 2009 +0200
    12.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 20 16:13:01 2009 +0200
    12.3 @@ -308,7 +308,7 @@
    12.4    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
    12.5    | _ => (acc, dacc)
    12.6    val (cs,ds) = h ([],[]) p
    12.7 -  val l = Integer.lcms (cs union ds)
    12.8 +  val l = Integer.lcms (gen_union (op =) (cs, ds))
    12.9    fun cv k ct =
   12.10      let val (tm as b$s$t) = term_of ct
   12.11      in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
    13.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Oct 20 13:37:56 2009 +0200
    13.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Oct 20 16:13:01 2009 +0200
    13.3 @@ -202,15 +202,15 @@
    13.4              val dupTs = map snd (duplicates (op =) vTs) @
    13.5                map_filter (AList.lookup (op =) vTs) vs;
    13.6            in
    13.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
    13.8 +            gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
    13.9              forall (is_eqT o fastype_of) in_ts' andalso
   13.10 -            term_vs t subset vs andalso
   13.11 +            gen_subset (op =) (term_vs t, vs) andalso
   13.12              forall is_eqT dupTs
   13.13            end)
   13.14              (if is_set then [Mode (([], []), [], [])]
   13.15               else modes_of modes t handle Option =>
   13.16                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   13.17 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   13.18 +      | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
   13.19            else NONE) ps);
   13.20  
   13.21  fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
   13.22 @@ -222,7 +222,7 @@
   13.23        | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
   13.24            NONE => NONE
   13.25          | SOME (x, _) => check_mode_prems
   13.26 -            (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
   13.27 +            (case x of Prem (us, _, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
   13.28              (filter_out (equal x) ps));
   13.29      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
   13.30      val in_vs = terms_vs in_ts;
   13.31 @@ -230,9 +230,9 @@
   13.32    in
   13.33      forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   13.34      forall (is_eqT o fastype_of) in_ts' andalso
   13.35 -    (case check_mode_prems (arg_vs union in_vs) ps of
   13.36 +    (case check_mode_prems (gen_union (op =) (arg_vs, in_vs)) ps of
   13.37         NONE => false
   13.38 -     | SOME vs => concl_vs subset vs)
   13.39 +     | SOME vs => gen_subset (op =) (concl_vs, vs))
   13.40    end;
   13.41  
   13.42  fun check_modes_pred thy arg_vs preds modes (p, ms) =
   13.43 @@ -482,7 +482,7 @@
   13.44  fun constrain cs [] = []
   13.45    | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
   13.46        NONE => xs
   13.47 -    | SOME xs' => xs inter xs') :: constrain cs ys;
   13.48 +    | SOME xs' => gen_inter (op =) (xs, xs')) :: constrain cs ys;
   13.49  
   13.50  fun mk_extra_defs thy defs gr dep names module ts =
   13.51    Library.foldl (fn (gr, name) =>
    14.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Oct 20 13:37:56 2009 +0200
    14.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Oct 20 16:13:01 2009 +0200
    14.3 @@ -209,7 +209,7 @@
    14.4        (case optf of
    14.5           NONE => fs
    14.6         | SOME f => AList.update op = (u, the_default f
    14.7 -           (Option.map (curry op inter f) (AList.lookup op = fs u))) fs));
    14.8 +           (Option.map (curry (gen_inter (op =)) f) (AList.lookup op = fs u))) fs));
    14.9  
   14.10  
   14.11  (**************************************************************)
    15.1 --- a/src/HOL/Tools/metis_tools.ML	Tue Oct 20 13:37:56 2009 +0200
    15.2 +++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 20 16:13:01 2009 +0200
    15.3 @@ -631,7 +631,7 @@
    15.4          let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
    15.5          in
    15.6             {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
    15.7 -            tfrees = tfree_lits union tfrees}
    15.8 +            tfrees = gen_union (op =) (tfree_lits, tfrees)}
    15.9          end;
   15.10        val lmap0 = List.foldl (add_thm true)
   15.11                          {axioms = [], tfrees = init_tfrees ctxt} cls
    16.1 --- a/src/HOL/Tools/old_primrec.ML	Tue Oct 20 13:37:56 2009 +0200
    16.2 +++ b/src/HOL/Tools/old_primrec.ML	Tue Oct 20 16:13:01 2009 +0200
    16.3 @@ -226,7 +226,7 @@
    16.4        (case Symtab.lookup dt_info tname of
    16.5            NONE => primrec_err (quote tname ^ " is not a datatype")
    16.6          | SOME dt =>
    16.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
    16.8 +            if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
    16.9                (tname, dt)::(find_dts dt_info tnames' tnames)
   16.10              else find_dts dt_info tnames' tnames);
   16.11  
    17.1 --- a/src/HOL/Tools/primrec.ML	Tue Oct 20 13:37:56 2009 +0200
    17.2 +++ b/src/HOL/Tools/primrec.ML	Tue Oct 20 16:13:01 2009 +0200
    17.3 @@ -208,7 +208,7 @@
    17.4        (case Symtab.lookup dt_info tname of
    17.5            NONE => primrec_error (quote tname ^ " is not a datatype")
    17.6          | SOME dt =>
    17.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
    17.8 +            if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
    17.9                (tname, dt)::(find_dts dt_info tnames' tnames)
   17.10              else find_dts dt_info tnames' tnames);
   17.11  
    18.1 --- a/src/HOL/Tools/prop_logic.ML	Tue Oct 20 13:37:56 2009 +0200
    18.2 +++ b/src/HOL/Tools/prop_logic.ML	Tue Oct 20 16:13:01 2009 +0200
    18.3 @@ -111,8 +111,8 @@
    18.4  	  | indices False            = []
    18.5  	  | indices (BoolVar i)      = [i]
    18.6  	  | indices (Not fm)         = indices fm
    18.7 -	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
    18.8 -	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
    18.9 +	  | indices (Or (fm1, fm2))  = gen_union (op =) (indices fm1, indices fm2)
   18.10 +	  | indices (And (fm1, fm2)) = gen_union (op =) (indices fm1, indices fm2);
   18.11  
   18.12  (* ------------------------------------------------------------------------- *)
   18.13  (* maxidx: computes the maximal variable index occuring in a formula of      *)
    19.1 --- a/src/HOL/Tools/record.ML	Tue Oct 20 13:37:56 2009 +0200
    19.2 +++ b/src/HOL/Tools/record.ML	Tue Oct 20 16:13:01 2009 +0200
    19.3 @@ -1834,7 +1834,7 @@
    19.4      val extN = full bname;
    19.5      val types = map snd fields;
    19.6      val alphas_fields = fold Term.add_tfree_namesT types [];
    19.7 -    val alphas_ext = alphas inter alphas_fields;
    19.8 +    val alphas_ext = gen_inter (op =) (alphas, alphas_fields);
    19.9      val len = length fields;
   19.10      val variants =
   19.11        Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
    20.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 20 13:37:56 2009 +0200
    20.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 20 16:13:01 2009 +0200
    20.3 @@ -1154,7 +1154,7 @@
    20.4        val axioms = collect_axioms thy u
    20.5        (* Term.typ list *)
    20.6        val types = Library.foldl (fn (acc, t') =>
    20.7 -        acc union (ground_types thy t')) ([], u :: axioms)
    20.8 +        gen_union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
    20.9        val _     = tracing ("Ground types: "
   20.10          ^ (if null types then "none."
   20.11             else commas (map (Syntax.string_of_typ_global thy) types)))
   20.12 @@ -2415,7 +2415,7 @@
   20.13                        (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
   20.14                    (* sanity check: typ_assoc must associate types to the   *)
   20.15                    (*               elements of 'dtyps' (and only to those) *)
   20.16 -                  val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
   20.17 +                  val _ = if not (gen_eq_set (op =) (dtyps, map fst typ_assoc))
   20.18                      then
   20.19                        raise REFUTE ("IDT_recursion_interpreter",
   20.20                          "type association has extra/missing elements")
   20.21 @@ -3007,7 +3007,7 @@
   20.22          [Type ("fun", [T, Type ("bool", [])]),
   20.23           Type ("fun", [_, Type ("bool", [])])]),
   20.24           Type ("fun", [_, Type ("bool", [])])])) =>
   20.25 -      let nonfix union (* because "union" is used below *)
   20.26 +      let
   20.27          val size_elem = size_of_type thy model T
   20.28          (* the universe (i.e. the set that contains every element) *)
   20.29          val i_univ = Node (replicate size_elem TT)
    21.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 20 13:37:56 2009 +0200
    21.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 20 16:13:01 2009 +0200
    21.3 @@ -213,8 +213,9 @@
    21.4          fun defs lhs rhs =
    21.5              let val (rator,args) = strip_comb lhs
    21.6                  val ct = const_with_typ thy (dest_ConstFree rator)
    21.7 -            in  forall is_Var args andalso uni_mem gctypes ct andalso
    21.8 -                Term.add_vars rhs [] subset Term.add_vars lhs []
    21.9 +            in
   21.10 +              forall is_Var args andalso uni_mem gctypes ct andalso
   21.11 +                gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
   21.12              end
   21.13              handle ConstFree => false
   21.14      in    
    22.1 --- a/src/HOL/Tools/res_clause.ML	Tue Oct 20 13:37:56 2009 +0200
    22.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Oct 20 16:13:01 2009 +0200
    22.3 @@ -93,7 +93,7 @@
    22.4  val tconst_prefix = "tc_";
    22.5  val class_prefix = "class_";
    22.6  
    22.7 -fun union_all xss = List.foldl (op union) [] xss;
    22.8 +fun union_all xss = List.foldl (gen_union (op =)) [] xss;
    22.9  
   22.10  (*Provide readable names for the more common symbolic functions*)
   22.11  val const_trans_table =
   22.12 @@ -263,7 +263,7 @@
   22.13    | pred_of_sort (LTFree (s,ty)) = (s,1)
   22.14  
   22.15  (*Given a list of sorted type variables, return a list of type literals.*)
   22.16 -fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts);
   22.17 +fun add_typs Ts = List.foldl (gen_union (op =)) [] (map sorts_on_typs Ts);
   22.18  
   22.19  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   22.20    * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   22.21 @@ -372,7 +372,7 @@
   22.22        let val cpairs = type_class_pairs thy tycons classes
   22.23            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
   22.24            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   22.25 -      in  (classes' union classes, cpairs' union cpairs)  end;
   22.26 +      in (gen_union (op =) (classes', classes), gen_union (op =) (cpairs', cpairs)) end;
   22.27  
   22.28  fun make_arity_clauses_dfg dfg thy tycons classes =
   22.29    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
    23.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 13:37:56 2009 +0200
    23.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 16:13:01 2009 +0200
    23.3 @@ -154,7 +154,7 @@
    23.4    | combterm_of dfg thy (P $ Q) =
    23.5        let val (P',tsP) = combterm_of dfg thy P
    23.6            val (Q',tsQ) = combterm_of dfg thy Q
    23.7 -      in  (CombApp(P',Q'), tsP union tsQ)  end
    23.8 +      in  (CombApp(P',Q'), gen_union (op =) (tsP, tsQ))  end
    23.9    | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
   23.10  
   23.11  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
   23.12 @@ -166,7 +166,7 @@
   23.13    | literals_of_term1 dfg thy (lits,ts) P =
   23.14        let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   23.15        in
   23.16 -          (Literal(pol,pred)::lits, ts union ts')
   23.17 +          (Literal(pol,pred)::lits, gen_union (op =) (ts, ts'))
   23.18        end;
   23.19  
   23.20  fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   23.21 @@ -475,7 +475,7 @@
   23.22      val (cma, cnh) = count_constants clauses
   23.23      val params = (t_full, cma, cnh)
   23.24      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   23.25 -    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
   23.26 +    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (gen_union (op =)) [] tfree_litss)
   23.27      val _ =
   23.28        File.write_list file (
   23.29          map (#1 o (clause2tptp params)) axclauses @
    24.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 20 13:37:56 2009 +0200
    24.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 20 16:13:01 2009 +0200
    24.3 @@ -364,7 +364,7 @@
    24.4  fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
    24.5  
    24.6  fun replace_deps (old:int, new) (lno, t, deps) =
    24.7 -      (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps));
    24.8 +      (lno, t, List.foldl (gen_union (op =)) [] (map (replace_dep (old, new)) deps));
    24.9  
   24.10  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   24.11    only in type information.*)
    25.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Oct 20 13:37:56 2009 +0200
    25.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Oct 20 16:13:01 2009 +0200
    25.3 @@ -471,8 +471,8 @@
    25.4          | forced_vars False             = []
    25.5          | forced_vars (BoolVar i)       = [i]
    25.6          | forced_vars (Not (BoolVar i)) = [~i]
    25.7 -        | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
    25.8 -        | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
    25.9 +        | forced_vars (Or (fm1, fm2))   = gen_inter (op =) (forced_vars fm1, forced_vars fm2)
   25.10 +        | forced_vars (And (fm1, fm2))  = gen_union (op =) (forced_vars fm1, forced_vars fm2)
   25.11          (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   25.12          (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   25.13          | forced_vars _                 = error "formula is not in negation normal form"
    26.1 --- a/src/HOL/Tools/transfer.ML	Tue Oct 20 13:37:56 2009 +0200
    26.2 +++ b/src/HOL/Tools/transfer.ML	Tue Oct 20 16:13:01 2009 +0200
    26.3 @@ -143,7 +143,7 @@
    26.4   {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
    26.5    ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
    26.6    hints = subtract (op = : string*string -> bool) hints0
    26.7 -            (hints1 union_string hints2)}
    26.8 +            (gen_union (op =) (hints1, hints2))}
    26.9   end;
   26.10  
   26.11  local
   26.12 @@ -151,7 +151,7 @@
   26.13  in
   26.14  fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
   26.15                     {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
   26.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}
   26.17 +    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = gen_union (op =) (hints1, hints2)}
   26.18  end;
   26.19  
   26.20  fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
    27.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Oct 20 13:37:56 2009 +0200
    27.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Oct 20 16:13:01 2009 +0200
    27.3 @@ -908,20 +908,20 @@
    27.4              val dupTs = map snd (duplicates (op =) vTs) @
    27.5                map_filter (AList.lookup (op =) vTs) vs;
    27.6            in
    27.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
    27.8 +            gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
    27.9              forall (is_eqT o fastype_of) in_ts' andalso
   27.10 -            term_vs t subset vs andalso
   27.11 +            gen_subset (op =) (term_vs t, vs) andalso
   27.12              forall is_eqT dupTs
   27.13            end)
   27.14              (modes_of_term modes t handle Option =>
   27.15                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   27.16        | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
   27.17              length us = length is andalso
   27.18 -            terms_vs us subset vs andalso
   27.19 -            term_vs t subset vs)
   27.20 +            gen_subset (op =) (terms_vs us, vs) andalso
   27.21 +            gen_subset (op =) (term_vs t, vs)
   27.22              (modes_of_term modes t handle Option =>
   27.23                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   27.24 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   27.25 +      | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
   27.26            else NONE
   27.27        ) ps);
   27.28  
   27.29 @@ -964,22 +964,22 @@
   27.30              (if with_generator then
   27.31                (case select_mode_prem thy gen_modes' vs ps of
   27.32                    SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
   27.33 -                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   27.34 +                  (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
   27.35                    (filter_out (equal p) ps)
   27.36                  | NONE =>
   27.37                    let 
   27.38                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
   27.39                    in
   27.40                      case (find_first (fn generator_vs => is_some
   27.41 -                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
   27.42 +                      (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
   27.43                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
   27.44 -                        (vs union generator_vs) ps
   27.45 +                        (gen_union (op =) (vs, generator_vs)) ps
   27.46                      | NONE => NONE
   27.47                    end)
   27.48              else
   27.49                NONE)
   27.50          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
   27.51 -            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   27.52 +            (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
   27.53              (filter_out (equal p) ps))
   27.54      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
   27.55      val in_vs = terms_vs in_ts;
   27.56 @@ -987,13 +987,13 @@
   27.57    in
   27.58      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   27.59      forall (is_eqT o fastype_of) in_ts' then
   27.60 -      case check_mode_prems [] (param_vs union in_vs) ps of
   27.61 +      case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
   27.62           NONE => NONE
   27.63         | SOME (acc_ps, vs) =>
   27.64           if with_generator then
   27.65             SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
   27.66           else
   27.67 -           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
   27.68 +           if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
   27.69      else NONE
   27.70    end;
   27.71  
    28.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Oct 20 13:37:56 2009 +0200
    28.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Oct 20 16:13:01 2009 +0200
    28.3 @@ -59,8 +59,8 @@
    28.4              fun analyse indirect (TFree(v,s))  =
    28.5                  (case AList.lookup (op =) tvars v of 
    28.6                     NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
    28.7 -                 | SOME sort => if eq_set_string (s,defaultS) orelse
    28.8 -                                   eq_set_string (s,sort    )
    28.9 +                 | SOME sort => if gen_eq_set (op =) (s, defaultS) orelse
   28.10 +                                   gen_eq_set (op =) (s, sort)
   28.11                                  then TFree(v,sort)
   28.12                                  else error ("Inconsistent sort constraint" ^
   28.13                                              " for type variable " ^ quote v))
    29.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Tue Oct 20 13:37:56 2009 +0200
    29.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Tue Oct 20 16:13:01 2009 +0200
    29.3 @@ -74,7 +74,7 @@
    29.4  fun proc ss t =
    29.5    let val (divs,mods) = coll_div_mod t ([],[])
    29.6    in if null divs orelse null mods then NONE
    29.7 -     else case divs inter mods of
    29.8 +     else case gen_inter (op =) (divs, mods) of
    29.9              pq :: _ => SOME (cancel ss t pq)
   29.10            | [] => NONE
   29.11    end
    30.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 20 13:37:56 2009 +0200
    30.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 20 16:13:01 2009 +0200
    30.3 @@ -385,7 +385,7 @@
    30.4    let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
    30.5    if not (null eqs) then
    30.6       let val c =
    30.7 -           fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs []
    30.8 +           fold (fn Lineq(_,_,l,_) => fn cs => gen_union (op =) (l, cs)) eqs []
    30.9             |> filter (fn i => i <> 0)
   30.10             |> sort (int_ord o pairself abs)
   30.11             |> hd
    31.1 --- a/src/Pure/General/name_space.ML	Tue Oct 20 13:37:56 2009 +0200
    31.2 +++ b/src/Pure/General/name_space.ML	Tue Oct 20 16:13:01 2009 +0200
    31.3 @@ -145,7 +145,7 @@
    31.4        space
    31.5        |> add_name' name name
    31.6        |> fold (del_name name)
    31.7 -        (if fully then names else names inter_string [Long_Name.base_name name])
    31.8 +        (if fully then names else gen_inter (op =) (names, [Long_Name.base_name name]))
    31.9        |> fold (del_name_extra name) (get_accesses space name)
   31.10      end;
   31.11  
    32.1 --- a/src/Pure/General/ord_list.ML	Tue Oct 20 13:37:56 2009 +0200
    32.2 +++ b/src/Pure/General/ord_list.ML	Tue Oct 20 16:13:01 2009 +0200
    32.3 @@ -56,7 +56,6 @@
    32.4  
    32.5  (* lists as sets *)
    32.6  
    32.7 -nonfix subset;
    32.8  fun subset ord (list1, list2) =
    32.9    let
   32.10      fun sub [] _ = true
   32.11 @@ -75,7 +74,6 @@
   32.12  fun handle_same f x = f x handle SAME => x;
   32.13  
   32.14  (*union: insert elements of first list into second list*)
   32.15 -nonfix union;
   32.16  fun union ord list1 list2 =
   32.17    let
   32.18      fun unio [] _ = raise SAME
   32.19 @@ -88,7 +86,6 @@
   32.20    in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
   32.21  
   32.22  (*intersection: filter second list for elements present in first list*)
   32.23 -nonfix inter;
   32.24  fun inter ord list1 list2 =
   32.25    let
   32.26      fun intr _ [] = raise SAME
    33.1 --- a/src/Pure/General/path.ML	Tue Oct 20 13:37:56 2009 +0200
    33.2 +++ b/src/Pure/General/path.ML	Tue Oct 20 16:13:01 2009 +0200
    33.3 @@ -42,7 +42,7 @@
    33.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
    33.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    33.6    | check_elem chs =
    33.7 -      (case ["/", "\\", "$", ":"] inter_string chs of
    33.8 +      (case gen_inter (op =) (["/", "\\", "$", ":"], chs) of
    33.9          [] => chs
   33.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
   33.11  
    34.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Oct 20 13:37:56 2009 +0200
    34.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Oct 20 16:13:01 2009 +0200
    34.3 @@ -289,7 +289,7 @@
    34.4      val _ = message "Collecting constraints...";
    34.5      val (t, prf, cs, env, _) = make_constraints_cprf thy
    34.6        (Envir.empty (maxidx_proof cprf ~1)) cprf';
    34.7 -    val cs' = map (fn p => (true, p, op union
    34.8 +    val cs' = map (fn p => (true, p, gen_union (op =) 
    34.9          (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
   34.10        (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
   34.11      val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
    35.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Oct 20 13:37:56 2009 +0200
    35.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Oct 20 16:13:01 2009 +0200
    35.3 @@ -77,7 +77,7 @@
    35.4    |> command K.prf_asm_goal     goal
    35.5    |> command K.prf_script       proofstep;
    35.6  
    35.7 -val _ = OuterKeyword.kinds subset_string Symtab.keys command_keywords
    35.8 +val _ = gen_subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
    35.9    orelse sys_error "Incomplete coverage of command keywords";
   35.10  
   35.11  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    36.1 --- a/src/Pure/Syntax/ast.ML	Tue Oct 20 13:37:56 2009 +0200
    36.2 +++ b/src/Pure/Syntax/ast.ML	Tue Oct 20 16:13:01 2009 +0200
    36.3 @@ -104,7 +104,7 @@
    36.4      val rvars = add_vars rhs [];
    36.5    in
    36.6      if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
    36.7 -    else if not (rvars subset lvars) then SOME "rhs contains extra variables"
    36.8 +    else if not (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
    36.9      else NONE
   36.10    end;
   36.11  
    37.1 --- a/src/Pure/Syntax/parser.ML	Tue Oct 20 13:37:56 2009 +0200
    37.2 +++ b/src/Pure/Syntax/parser.ML	Tue Oct 20 16:13:01 2009 +0200
    37.3 @@ -147,7 +147,7 @@
    37.4                      in
    37.5                        if member (op =) nts l then       (*update production's lookahead*)
    37.6                        let
    37.7 -                        val new_lambda = is_none tk andalso nts subset lambdas;
    37.8 +                        val new_lambda = is_none tk andalso gen_subset (op =) (nts, lambdas);
    37.9  
   37.10                          val new_tks = subtract (op =) l_starts
   37.11                            ((if is_some tk then [the tk] else []) @
    38.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Oct 20 13:37:56 2009 +0200
    38.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Oct 20 16:13:01 2009 +0200
    38.3 @@ -352,7 +352,7 @@
    38.4    in
    38.5      SynExt {
    38.6        xprods = xprods,
    38.7 -      consts = consts union_string mfix_consts,
    38.8 +      consts = gen_union (op =) (consts, mfix_consts),
    38.9        prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
   38.10        parse_ast_translation = parse_ast_translation,
   38.11        parse_rules = parse_rules' @ parse_rules,
    39.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Oct 20 13:37:56 2009 +0200
    39.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Oct 20 16:13:01 2009 +0200
    39.3 @@ -227,7 +227,7 @@
    39.4  
    39.5      fun check (t, NONE) = check (t, SOME (get_thm_names t))
    39.6        | check ((_, thm), c as SOME thm_consts) =
    39.7 -         (if pat_consts subset_string thm_consts andalso
    39.8 +         (if gen_subset (op =) (pat_consts, thm_consts) andalso
    39.9              Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
   39.10            then SOME (0, 0) else NONE, c);
   39.11    in check end;
    40.1 --- a/src/Pure/codegen.ML	Tue Oct 20 13:37:56 2009 +0200
    40.2 +++ b/src/Pure/codegen.ML	Tue Oct 20 16:13:01 2009 +0200
    40.3 @@ -599,8 +599,8 @@
    40.4       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
    40.5  
    40.6  fun new_names t xs = Name.variant_list
    40.7 -  (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
    40.8 -    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
    40.9 +  (gen_union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
   40.10 +    OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
   40.11  
   40.12  fun new_name t x = hd (new_names t [x]);
   40.13  
    41.1 --- a/src/Pure/library.ML	Tue Oct 20 13:37:56 2009 +0200
    41.2 +++ b/src/Pure/library.ML	Tue Oct 20 16:13:01 2009 +0200
    41.3 @@ -11,8 +11,7 @@
    41.4  infix 2 ?
    41.5  infix 3 o oo ooo oooo
    41.6  infix 4 ~~ upto downto
    41.7 -infix orf andf \ \\ mem mem_int mem_string union union_int
    41.8 -  union_string inter inter_int inter_string subset subset_int subset_string
    41.9 +infix orf andf \ \\ mem mem_int mem_string
   41.10  
   41.11  signature BASIC_LIBRARY =
   41.12  sig
   41.13 @@ -163,19 +162,8 @@
   41.14    val mem: ''a * ''a list -> bool
   41.15    val mem_int: int * int list -> bool
   41.16    val mem_string: string * string list -> bool
   41.17 -  val union: ''a list * ''a list -> ''a list
   41.18 -  val union_int: int list * int list -> int list
   41.19 -  val union_string: string list * string list -> string list
   41.20    val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   41.21    val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   41.22 -  val inter: ''a list * ''a list -> ''a list
   41.23 -  val inter_int: int list * int list -> int list
   41.24 -  val inter_string: string list * string list -> string list
   41.25 -  val subset: ''a list * ''a list -> bool
   41.26 -  val subset_int: int list * int list -> bool
   41.27 -  val subset_string: string list * string list -> bool
   41.28 -  val eq_set: ''a list * ''a list -> bool
   41.29 -  val eq_set_string: string list * string list -> bool
   41.30    val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   41.31    val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   41.32    val \ : ''a list * ''a -> ''a list
   41.33 @@ -811,70 +799,20 @@
   41.34  fun (x: string) mem_string xs = member (op =) xs x;
   41.35  
   41.36  (*union of sets represented as lists: no repetitions*)
   41.37 -fun xs union [] = xs
   41.38 -  | [] union ys = ys
   41.39 -  | (x :: xs) union ys = xs union (insert (op =) x ys);
   41.40 -
   41.41 -(*union of sets, optimized version for ints*)
   41.42 -fun (xs:int list) union_int [] = xs
   41.43 -  | [] union_int ys = ys
   41.44 -  | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
   41.45 -
   41.46 -(*union of sets, optimized version for strings*)
   41.47 -fun (xs:string list) union_string [] = xs
   41.48 -  | [] union_string ys = ys
   41.49 -  | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
   41.50 -
   41.51 -(*generalized union*)
   41.52  fun gen_union eq (xs, []) = xs
   41.53    | gen_union eq ([], ys) = ys
   41.54    | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
   41.55  
   41.56 -
   41.57  (*intersection*)
   41.58 -fun [] inter ys = []
   41.59 -  | (x :: xs) inter ys =
   41.60 -      if x mem ys then x :: (xs inter ys) else xs inter ys;
   41.61 -
   41.62 -(*intersection, optimized version for ints*)
   41.63 -fun ([]:int list) inter_int ys = []
   41.64 -  | (x :: xs) inter_int ys =
   41.65 -      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
   41.66 -
   41.67 -(*intersection, optimized version for strings *)
   41.68 -fun ([]:string list) inter_string ys = []
   41.69 -  | (x :: xs) inter_string ys =
   41.70 -      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
   41.71 -
   41.72 -(*generalized intersection*)
   41.73  fun gen_inter eq ([], ys) = []
   41.74    | gen_inter eq (x::xs, ys) =
   41.75        if member eq ys x then x :: gen_inter eq (xs, ys)
   41.76        else gen_inter eq (xs, ys);
   41.77  
   41.78 -
   41.79  (*subset*)
   41.80 -fun [] subset ys = true
   41.81 -  | (x :: xs) subset ys = x mem ys andalso xs subset ys;
   41.82 -
   41.83 -(*subset, optimized version for ints*)
   41.84 -fun ([]: int list) subset_int ys = true
   41.85 -  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
   41.86 -
   41.87 -(*subset, optimized version for strings*)
   41.88 -fun ([]: string list) subset_string ys = true
   41.89 -  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
   41.90 +fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
   41.91  
   41.92  (*set equality*)
   41.93 -fun eq_set (xs, ys) =
   41.94 -  xs = ys orelse (xs subset ys andalso ys subset xs);
   41.95 -
   41.96 -(*set equality for strings*)
   41.97 -fun eq_set_string ((xs: string list), ys) =
   41.98 -  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
   41.99 -
  41.100 -fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
  41.101 -
  41.102  fun gen_eq_set eq (xs, ys) =
  41.103    eq_list eq (xs, ys) orelse
  41.104      (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
    42.1 --- a/src/Pure/meta_simplifier.ML	Tue Oct 20 13:37:56 2009 +0200
    42.2 +++ b/src/Pure/meta_simplifier.ML	Tue Oct 20 16:13:01 2009 +0200
    42.3 @@ -864,7 +864,7 @@
    42.4    while the premises are solved.*)
    42.5  
    42.6  fun cond_skel (args as (_, (lhs, rhs))) =
    42.7 -  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
    42.8 +  if gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
    42.9    else skel0;
   42.10  
   42.11  (*
    43.1 --- a/src/Pure/pattern.ML	Tue Oct 20 13:37:56 2009 +0200
    43.2 +++ b/src/Pure/pattern.ML	Tue Oct 20 16:13:01 2009 +0200
    43.3 @@ -216,10 +216,10 @@
    43.4  
    43.5  fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
    43.6    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    43.7 -            if js subset_int is
    43.8 +            if gen_subset (op =) (js, is)
    43.9              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
   43.10                   in Envir.update (((F, Fty), t), env) end
   43.11 -            else let val ks = is inter_int js
   43.12 +            else let val ks = gen_inter (op =) (is, js)
   43.13                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
   43.14                       val (env',H) = Envir.genvar a (env,Hty)
   43.15                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
   43.16 @@ -339,7 +339,7 @@
   43.17    let val js = loose_bnos t
   43.18    in if null is
   43.19       then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
   43.20 -     else if js subset_int is
   43.21 +     else if gen_subset (op =) (js, is)
   43.22            then let val t' = if downto0(is,length binders - 1) then t
   43.23                              else mapbnd (idx is) t
   43.24                 in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end
    44.1 --- a/src/Pure/proofterm.ML	Tue Oct 20 13:37:56 2009 +0200
    44.2 +++ b/src/Pure/proofterm.ML	Tue Oct 20 16:13:01 2009 +0200
    44.3 @@ -900,8 +900,8 @@
    44.4  
    44.5  fun add_funvars Ts (vs, t) =
    44.6    if is_fun (fastype_of1 (Ts, t)) then
    44.7 -    vs union map_filter (fn Var (ixn, T) =>
    44.8 -      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)
    44.9 +    gen_union (op =) (vs, map_filter (fn Var (ixn, T) =>
   44.10 +      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
   44.11    else vs;
   44.12  
   44.13  fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
   44.14 @@ -918,7 +918,7 @@
   44.15    | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   44.16    | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
   44.17  
   44.18 -fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
   44.19 +fun prop_vars (Const ("==>", _) $ P $ Q) = gen_union (op =) (prop_vars P, prop_vars Q)
   44.20    | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
   44.21    | prop_vars t = (case strip_comb t of
   44.22        (Var (ixn, _), _) => [ixn] | _ => []);
   44.23 @@ -936,9 +936,9 @@
   44.24    end;
   44.25  
   44.26  fun needed_vars prop =
   44.27 -  Library.foldl (op union)
   44.28 -    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
   44.29 -  prop_vars prop;
   44.30 +  gen_union (op =) (Library.foldl (gen_union (op =))
   44.31 +    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
   44.32 +  prop_vars prop);
   44.33  
   44.34  fun gen_axm_proof c name prop =
   44.35    let
   44.36 @@ -975,7 +975,7 @@
   44.37            let
   44.38              val p as (_, is', ch', prf') = shrink ls lev prf2;
   44.39              val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
   44.40 -          in (is union is', ch orelse ch', ts',
   44.41 +          in (gen_union (op =) (is, is'), ch orelse ch', ts',
   44.42                if ch orelse ch' then prf'' %% prf' else prf)
   44.43            end
   44.44        | shrink' ls lev ts prfs (prf as prf1 % t) =
   44.45 @@ -1004,15 +1004,15 @@
   44.46              val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
   44.47              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
   44.48                insert (op =) ixn (case AList.lookup (op =) insts ixn of
   44.49 -                  SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
   44.50 -                | _ => ixns union ixns'))
   44.51 +                  SOME (SOME t) => if is_proj t then gen_union (op =) (ixns, ixns') else ixns'
   44.52 +                | _ => gen_union (op =) (ixns, ixns')))
   44.53                    (needed prop ts'' prfs, add_npvars false true [] ([], prop));
   44.54              val insts' = map
   44.55                (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
   44.56                  | (_, x) => (false, x)) insts
   44.57            in ([], false, insts' @ map (pair false) ts'', prf) end
   44.58      and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
   44.59 -          (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
   44.60 +          gen_union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
   44.61        | needed (Var (ixn, _)) (_::_) _ = [ixn]
   44.62        | needed _ _ _ = [];
   44.63    in shrink end;
    45.1 --- a/src/Pure/sorts.ML	Tue Oct 20 13:37:56 2009 +0200
    45.2 +++ b/src/Pure/sorts.ML	Tue Oct 20 16:13:01 2009 +0200
    45.3 @@ -72,8 +72,8 @@
    45.4  (** ordered lists of sorts **)
    45.5  
    45.6  val make = OrdList.make TermOrd.sort_ord;
    45.7 -val op subset = OrdList.subset TermOrd.sort_ord;
    45.8 -val op union = OrdList.union TermOrd.sort_ord;
    45.9 +val subset = OrdList.subset TermOrd.sort_ord;
   45.10 +val union = OrdList.union TermOrd.sort_ord;
   45.11  val subtract = OrdList.subtract TermOrd.sort_ord;
   45.12  
   45.13  val remove_sort = OrdList.remove TermOrd.sort_ord;
    46.1 --- a/src/Pure/thm.ML	Tue Oct 20 13:37:56 2009 +0200
    46.2 +++ b/src/Pure/thm.ML	Tue Oct 20 16:13:01 2009 +0200
    46.3 @@ -1463,7 +1463,7 @@
    46.4      (case duplicates (op =) cs of
    46.5        a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
    46.6      | [] =>
    46.7 -      (case cs inter_string freenames of
    46.8 +      (case gen_inter (op =) (cs, freenames) of
    46.9          a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
   46.10        | [] =>
   46.11          Thm (der,
    47.1 --- a/src/Pure/variable.ML	Tue Oct 20 13:37:56 2009 +0200
    47.2 +++ b/src/Pure/variable.ML	Tue Oct 20 16:13:01 2009 +0200
    47.3 @@ -301,7 +301,7 @@
    47.4      val names = names_of ctxt;
    47.5      val (xs', names') =
    47.6        if is_body ctxt then Name.variants xs names |>> map Name.skolem
    47.7 -      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs);
    47.8 +      else (no_dups (gen_inter (op =) (xs, ys)); no_dups (gen_inter (op =) (xs, zs));
    47.9          (xs, fold Name.declare xs names));
   47.10    in ctxt |> new_fixes names' xs xs' end;
   47.11  
    48.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Tue Oct 20 13:37:56 2009 +0200
    48.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Tue Oct 20 16:13:01 2009 +0200
    48.3 @@ -139,13 +139,13 @@
    48.4        val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
    48.5        val (conds_tyvs,cond_vs) = 
    48.6            Library.foldl (fn ((tyvs, vs), t) => 
    48.7 -                    (Library.union
    48.8 +                    (gen_union (op =)
    48.9                         (OldTerm.term_tvars t, tyvs),
   48.10 -                     Library.union 
   48.11 +                     gen_union (op =)
   48.12                         (map Term.dest_Var (OldTerm.term_vars t), vs))) 
   48.13                  (([],[]), rule_conds);
   48.14        val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
   48.15 -      val vars_to_fix = Library.union (termvars, cond_vs);
   48.16 +      val vars_to_fix = gen_union (op =) (termvars, cond_vs);
   48.17        val (renamings, names2) = 
   48.18            List.foldr (fn (((n,i),ty), (vs, names')) => 
   48.19                      let val n' = Name.variant names' n in
    49.1 --- a/src/Tools/Metis/metis_env.ML	Tue Oct 20 13:37:56 2009 +0200
    49.2 +++ b/src/Tools/Metis/metis_env.ML	Tue Oct 20 16:13:01 2009 +0200
    49.3 @@ -1,5 +1,5 @@
    49.4  (* Metis-specific ML environment *)
    49.5 -nonfix ++ -- RL mem union subset;
    49.6 +nonfix ++ -- RL mem;
    49.7  val explode = String.explode;
    49.8  val implode = String.implode;
    49.9  val print = TextIO.print;
    50.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Oct 20 13:37:56 2009 +0200
    50.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Oct 20 16:13:01 2009 +0200
    50.3 @@ -65,7 +65,7 @@
    50.4    in
    50.5      if has_duplicates (op =) lfrees then
    50.6        raise RecError "repeated variable name in pattern"
    50.7 -    else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
    50.8 +    else if not (gen_subset (op =) (Term.add_frees rhs [], lfrees)) then
    50.9        raise RecError "extra variables on rhs"
   50.10      else if length middle > 1 then
   50.11        raise RecError "more than one non-variable in pattern"