src/HOL/Nominal/nominal_package.ML
changeset 18759 2f55e3e47355
parent 18707 9d6154f76476
child 19133 7e84a1a3741c
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Jan 23 15:14:06 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Jan 23 15:23:31 2006 +0100
     1.3 @@ -428,13 +428,13 @@
     1.4          (List.take (descr, length new_type_names)) |>
     1.5        PureThy.add_thmss
     1.6          [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
     1.7 -          unfolded_perm_eq_thms), [Attrib.theory Simplifier.simp_add]),
     1.8 +          unfolded_perm_eq_thms), [Simplifier.simp_add]),
     1.9           ((space_implode "_" new_type_names ^ "_perm_empty",
    1.10 -          perm_empty_thms), [Attrib.theory Simplifier.simp_add]),
    1.11 +          perm_empty_thms), [Simplifier.simp_add]),
    1.12           ((space_implode "_" new_type_names ^ "_perm_append",
    1.13 -          perm_append_thms), [Attrib.theory Simplifier.simp_add]),
    1.14 +          perm_append_thms), [Simplifier.simp_add]),
    1.15           ((space_implode "_" new_type_names ^ "_perm_eq",
    1.16 -          perm_eq_thms), [Attrib.theory Simplifier.simp_add])];
    1.17 +          perm_eq_thms), [Simplifier.simp_add])];
    1.18    
    1.19      (**** Define representing sets ****)
    1.20  
    1.21 @@ -1071,7 +1071,7 @@
    1.22           length new_type_names))
    1.23        end) atoms;
    1.24  
    1.25 -    val simp_atts = replicate (length new_type_names) [Attrib.theory Simplifier.simp_add];
    1.26 +    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
    1.27  
    1.28      val (_, thy9) = thy8 |>
    1.29        Theory.add_path big_name |>