src/HOL/Nominal/nominal_package.ML

                  if null dts then Const ("{}", HOLogic.mk_setT atomT)
                  else foldr1 (HOLogic.mk_binop "op Un") (map supp args2)))))
             (fn _ =>
               [simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
+                 refl :: symmetric empty_def :: Finites.emptyI :: simp_thms @
                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1])
         in
           (supp_thm,
            prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
               (fresh c,