# HG changeset patch
# User berghofe
# Date 1129566891 -7200
# Node ID 09236f6a6a194448dc61c615ba5467be6ab1cbdc
# Parent  f08fc98a164aeddd4b24331f83b547d857b77de0
Fixed bug in proof of support theorem (it failed on constructors with no arguments).

diff -r f08fc98a164a -r 09236f6a6a19 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 17:42:24 2005 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 18:34:51 2005 +0200
@@ -1769,6 +1769,7 @@
             (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,