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 18759 2f55e3e47355
parent 18707 9d6154f76476
child 19133 7e84a1a3741c 
--- a/src/HOL/Nominal/nominal_package.ML	Mon Jan 23 15:14:06 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Jan 23 15:23:31 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), [Attrib.theory Simplifier.simp_add]),
+          unfolded_perm_eq_thms), [Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_empty",
-          perm_empty_thms), [Attrib.theory Simplifier.simp_add]),
+          perm_empty_thms), [Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_append",
-          perm_append_thms), [Attrib.theory Simplifier.simp_add]),
+          perm_append_thms), [Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_eq",
-          perm_eq_thms), [Attrib.theory Simplifier.simp_add])];
+          perm_eq_thms), [Simplifier.simp_add])];
   
     (**** Define representing sets ****)
 
@@ -1071,7 +1071,7 @@
          length new_type_names))
       end) atoms;
 
-    val simp_atts = replicate (length new_type_names) [Attrib.theory Simplifier.simp_add];
+    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
 
     val (_, thy9) = thy8 |>
       Theory.add_path big_name |>
isabelle