src/HOL/ex/predicate_compile.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
-            gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
+            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
             forall (is_eqT o fastype_of) in_ts' andalso
-            gen_subset (op =) (term_vs t, 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
-            gen_subset (op =) (terms_vs us, vs) andalso
-            gen_subset (op =) (term_vs t, 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 gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
+      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
           else NONE
       ) ps);
 
 fun fold_prem f (Prem (args, _)) = fold f args
   | fold_prem f (Negprem (args, _)) = fold f args

       | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of
           NONE =>
             (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, _) => gen_union (op =) (vs, 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' (gen_union (op =) (vs, 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)
-                        (gen_union (op =) (vs, 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, _) => gen_union (op =) (vs, 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;
     val concl_vs = terms_vs ts
   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 [] (gen_union (op =) (param_vs, 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 gen_subset (op =) (concl_vs, 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;
 
 fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
   let val SOME rs = AList.lookup (op =) preds p