Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_package.ML
changeset 18707 9d6154f76476
parent 18658 317a6f0ef8b9
child 18759 2f55e3e47355 
--- 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 |>
isabelle