# HG changeset patch
# User urbanc
# Date 1131370525 -3600
# Node ID dbe58b104cb9e0bc63f1e7f6ef7c71f1f7d29f13
# Parent  7a524bfa8d65d285c6f6b1d750693a2339e15147
added thms perm, distinct and fresh to the simplifier.
One would liket to add also inject, but this causes
problems with "congruences" like

  Lam [a].t1 = Lam [b].t2
  P (Lam [a].t1)
  -----------------------
  P (Lam [b].t2)


because the equation "Lam [a].t1 = Lam [b].t2" would simplify
to "[a].t1 = [b].t2" and then the goal is not true just by
simplification.

diff -r 7a524bfa8d65 -r dbe58b104cb9 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Mon Nov 07 12:06:11 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Nov 07 14:35:25 2005 +0100
@@ -1011,16 +1011,18 @@
          length new_type_names))
       end) atoms;
 
+    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
+
     val (thy9, _) = thy8 |>
       Theory.add_path big_name |>
       PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
       Theory.parent_path |>>>
-      DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
+      DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms |>>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
-      DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
+      DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' |>>>
       DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
       DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
-      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms |>>
+      DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms |>>
       fold (fn (atom, ths) => fn thy =>
         let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
         in fold (fn T => AxClass.add_inst_arity_i