src/HOL/Tools/inductive_codegen.ML

             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
             val vTs = maps term_vTs out_ts';
             val dupTs = map snd (duplicates (op =) vTs) @
               map_filter (AList.lookup (op =) vTs) vs;
           in
-            terms_vs (in_ts @ in_ts') subset vs andalso
+            gen_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
+            gen_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 gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
           else NONE) ps);
 
 fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
   let
     val modes' = modes @ map_filter

         (arg_vs ~~ iss);
     fun check_mode_prems vs [] = SOME vs
       | 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, _, _) => gen_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;
     val concl_vs = terms_vs ts
   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 (gen_union (op =) (arg_vs, in_vs)) ps of
        NONE => false
-     | SOME vs => concl_vs subset vs)
+     | SOME vs => gen_subset (op =) (concl_vs, vs))
   end;
 
 fun check_modes_pred thy arg_vs preds modes (p, ms) =
   let val SOME rs = AList.lookup (op =) preds p
   in (p, List.filter (fn m => case find_index

 fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
 
 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' => gen_inter (op =) (xs, xs')) :: constrain cs ys;
 
 fun mk_extra_defs thy defs gr dep names module ts =
   Library.foldl (fn (gr, name) =>
     if name mem names then gr
     else (case get_clauses thy name of