src/HOL/Nominal/nominal_datatype.ML

       (perm_indnames ~~ descr);
 
     fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
       (List.take (split_conj_thm (Goal.prove_global thy4 [] []
         (augment_sort thy4
-          (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
+          (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
             (fn ((s, T), x) =>
                let
                  val S = Const (s, T --> HOLogic.boolT);
                  val permT = mk_permT (Type (name, []))

       fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
         perm_def), name), tvs), perm_closed) => fn thy =>
           let
             val pt_class = pt_class_of thy atom;
             val sort = Sign.certify_sort thy
-              (pt_class :: map (cp_class_of thy atom) (dt_atoms \ atom))
+              (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms))
           in AxClass.prove_arity
             (Sign.intern_type thy name,
               map (inter_sort thy sort o snd) tvs, [pt_class])
             (EVERY [Class.intro_classes_tac [],
               rewrite_goals_tac [perm_def],

 
     fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
       let
         val cp_class = cp_class_of thy atom1 atom2;
         val sort = Sign.certify_sort thy
-          (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (dt_atoms \ atom1) @
+          (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
            (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
-            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (dt_atoms \ atom2)));
+            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms)));
         val cp1' = cp_inst_of thy atom1 atom2 RS cp1
       in fold (fn ((((((Abs_inverse, Rep),
         perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
           AxClass.prove_arity
             (Sign.intern_type thy name,

         val permT = mk_permT (Type (atom, []));
         val pi = Free ("pi", permT);
       in
         Goal.prove_global thy8 [] []
           (augment_sort thy8
-            (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
+            (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
             (HOLogic.mk_Trueprop (HOLogic.mk_eq
               (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
                Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
           (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
             perm_closed_thms @ Rep_thms)) 1)

           val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
           val c = Const (cname, map fastype_of l_args ---> T)
         in
           Goal.prove_global thy8 [] []
             (augment_sort thy8
-              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
+              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
               (HOLogic.mk_Trueprop (HOLogic.mk_eq
                 (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
             (fn _ => EVERY
               [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
                simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @

     val alpha = PureThy.get_thms thy8 "alpha";
     val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
 
     val pt_cp_sort =
       map (pt_class_of thy8) dt_atoms @
-      maps (fn s => map (cp_class_of thy8 s) (dt_atoms \ s)) dt_atoms;
+      maps (fn s => map (cp_class_of thy8 s) (remove (op =) s dt_atoms)) dt_atoms;
 
     val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
       let val T = nth_dtyp' i
       in map_filter (fn ((cname, dts), constr_rep_thm) =>
         if null dts then NONE else SOME

           [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th
       end;
 
     val fs_cp_sort =
       map (fs_class_of thy9) dt_atoms @
-      maps (fn s => map (cp_class_of thy9 s) (dt_atoms \ s)) dt_atoms;
+      maps (fn s => map (cp_class_of thy9 s) (remove (op =) s dt_atoms)) dt_atoms;
 
     (**********************************************************************
       The subgoals occurring in the proof of induct_aux have the
       following parameters: