src/HOL/Nominal/nominal_datatype.ML

 val In1_eq = thm "In1_eq";
 val In0_not_In1 = thm "In0_not_In1";
 val In1_not_In0 = thm "In1_not_In0";
 val Un_assoc = thm "Un_assoc";
 val Collect_disj_eq = thm "Collect_disj_eq";
-val empty_def = thm "empty_def";
+val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
 val empty_iff = thm "empty_iff";
 
 open DatatypeAux;
 open NominalAtoms;
 

                  if null dts then HOLogic.mk_set atomT []
                  else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
-                 symmetric empty_def :: finite_emptyI :: simp_thms @
+                 Collect_False_empty :: finite_emptyI :: simp_thms @
                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
         in
           (supp_thm,
            Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
              (HOLogic.mk_Trueprop (HOLogic.mk_eq