# HG changeset patch
# User berghofe
# Date 1188318011 -7200
# Node ID fd114392bca9e5b923477eb3452ea2f3f6c3e427
# Parent  83b6119078bc97de063356514b77e971c70995af
Got rid of large simpset in proof of characteristic equations
for freshness.

diff -r 83b6119078bc -r fd114392bca9 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Aug 28 18:16:06 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Aug 28 18:20:11 2007 +0200
@@ -33,6 +33,7 @@
 val Un_assoc = thm "Un_assoc";
 val Collect_disj_eq = thm "Collect_disj_eq";
 val empty_def = thm "empty_def";
+val empty_iff = thm "empty_iff";
 
 open DatatypeAux;
 open NominalAtoms;
@@ -1041,7 +1042,7 @@
                if null dts then HOLogic.true_const
                else foldr1 HOLogic.mk_conj (map fresh args2))))
              (fn _ =>
-               simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1))
+               simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
         end) atoms) constrs)
       end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));