src/HOL/Nominal/nominal_inductive.ML

     val ind_params = Inductive.params_of raw_induct;
     val raw_induct = atomize_induct ctxt raw_induct;
     val elims = map (atomize_induct ctxt) elims;
     val monos = Inductive.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
-    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
+    val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
     val induct_cases = map fst (fst (RuleCases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));

     val _ = (case duplicates (op = o pairself fst) avoids of
         [] => ()
       | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
     val _ = assert_all (null o duplicates op = o snd) avoids
       (fn (a, _) => error ("Duplicate variable names for case " ^ quote a));
-    val _ = (case map fst avoids \\ induct_cases of
+    val _ = (case subtract (op =) induct_cases (map fst avoids) of
         [] => ()
       | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
     val avoids' = if null induct_cases then replicate (length intrs) ("", [])
       else map (fn name =>
         (name, the_default [] (AList.lookup op = avoids name))) induct_cases;

       let val atoms = map (Sign.intern_type thy) xatoms
       in
         (case duplicates op = atoms of
              [] => ()
            | xs => error ("Duplicate atoms: " ^ commas xs);
-         case atoms \\ atoms' of
+         case subtract (op =) atoms' atoms of
              [] => ()
            | xs => error ("No such atoms: " ^ commas xs);
          atoms)
       end;
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";