# HG changeset patch
# User berghofe
# Date 1137681910 -3600
# Node ID 9d6154f76476a884d72036ce95291cb9cbd7665c
# Parent  1e7562c7afe64a757053b04a23140f1bbdb525f9
Use generic Simplifier.simp_add attribute instead
of Simplifier.simp_add_global.

diff -r 1e7562c7afe6 -r 9d6154f76476 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 19 14:59:55 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 19 15:45:10 2006 +0100
@@ -201,7 +201,7 @@
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
           AxClass.add_axclass_i (cl_name, ["HOL.type"])
-                [((cl_name^"1", axiom1),[Simplifier.simp_add_global]), 
+                [((cl_name^"1", axiom1),[Attrib.theory Simplifier.simp_add]), 
                  ((cl_name^"2", axiom2),[]),                           
                  ((cl_name^"3", axiom3),[])] thy                          
       end) ak_names_types thy6;
diff -r 1e7562c7afe6 -r 9d6154f76476 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Jan 19 14:59:55 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Jan 19 15:45:10 2006 +0100
@@ -428,13 +428,13 @@
         (List.take (descr, length new_type_names)) |>
       PureThy.add_thmss
         [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
-          unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
+          unfolded_perm_eq_thms), [Attrib.theory Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_empty",
-          perm_empty_thms), [Simplifier.simp_add_global]),
+          perm_empty_thms), [Attrib.theory Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_append",
-          perm_append_thms), [Simplifier.simp_add_global]),
+          perm_append_thms), [Attrib.theory Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_eq",
-          perm_eq_thms), [Simplifier.simp_add_global])];
+          perm_eq_thms), [Attrib.theory Simplifier.simp_add])];
   
     (**** Define representing sets ****)
 
@@ -1071,7 +1071,7 @@
          length new_type_names))
       end) atoms;
 
-    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
+    val simp_atts = replicate (length new_type_names) [Attrib.theory Simplifier.simp_add];
 
     val (_, thy9) = thy8 |>
       Theory.add_path big_name |>