src/HOL/Nominal/nominal_datatype.ML
changeset 32129 d2aea34845d4
parent 32124 954321008785
child 32134 ee143615019c
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 21 17:03:40 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 08:05:33 2009 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  val In1_not_In0 = thm "In1_not_In0";
     1.5  val Un_assoc = thm "Un_assoc";
     1.6  val Collect_disj_eq = thm "Collect_disj_eq";
     1.7 -val empty_def = thm "empty_def";
     1.8 +val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
     1.9  val empty_iff = thm "empty_iff";
    1.10  
    1.11  open DatatypeAux;
    1.12 @@ -1017,7 +1017,7 @@
    1.13              (fn _ =>
    1.14                simp_tac (HOL_basic_ss addsimps (supp_def ::
    1.15                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
    1.16 -                 symmetric empty_def :: finite_emptyI :: simp_thms @
    1.17 +                 Collect_False_empty :: finite_emptyI :: simp_thms @
    1.18                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
    1.19          in
    1.20            (supp_thm,