# HG changeset patch
# User haftmann
# Date 1248242733 -7200
# Node ID d2aea34845d42176187b9c36187d4326851ff29c
# Parent  59be4804c9ae5006ad9bd0fc70d416e9ccba2f5f
explicit antiquotation

diff -r 59be4804c9ae -r d2aea34845d4 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 21 17:03:40 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 08:05:33 2009 +0200
@@ -34,7 +34,7 @@
 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;
@@ -1017,7 +1017,7 @@
             (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,