--- 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,