src/HOL/Nominal/nominal_package.ML
changeset 18104 dbe58b104cb9
parent 18068 e8c3d371594e
child 18107 ee6b4d3af498
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Nov 07 12:06:11 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Nov 07 14:35:25 2005 +0100
     1.3 @@ -1011,16 +1011,18 @@
     1.4           length new_type_names))
     1.5        end) atoms;
     1.6  
     1.7 +    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
     1.8 +
     1.9      val (thy9, _) = thy8 |>
    1.10        Theory.add_path big_name |>
    1.11        PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
    1.12        Theory.parent_path |>>>
    1.13 -      DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
    1.14 +      DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms |>>>
    1.15        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
    1.16 -      DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
    1.17 +      DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' |>>>
    1.18        DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
    1.19        DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
    1.20 -      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms |>>
    1.21 +      DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms |>>
    1.22        fold (fn (atom, ths) => fn thy =>
    1.23          let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
    1.24          in fold (fn T => AxClass.add_inst_arity_i