src/HOL/Tools/inductive_package.ML
changeset 5891 92e0f5e6fd17
parent 5718 e5094d678285
child 6092 d9db67970c73
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Nov 16 11:13:28 1998 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Nov 16 11:14:02 1998 +0100
     1.3 @@ -464,9 +464,9 @@
     1.4        else standard (raw_induct RSN (2, rev_mp));
     1.5  
     1.6      val thy'' = thy' |>
     1.7 -      PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] |>
     1.8 +      PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
     1.9        (if no_elim then I else PureThy.add_tthmss
    1.10 -        [(("elims", map Attribute.tthm_of elims), [])]) |>
    1.11 +        [(("elims", Attribute.tthms_of elims), [])]) |>
    1.12        (if no_ind then I else PureThy.add_tthms
    1.13          [(((if coind then "co" else "") ^ "induct",
    1.14            Attribute.tthm_of induct), [])]) |>
    1.15 @@ -600,8 +600,8 @@
    1.16      val intr_ts'' = map subst intr_ts';
    1.17  
    1.18    in add_inductive_i verbose false "" coind false false cs'' intr_ts''
    1.19 -    (map (Attribute.thm_of) (PureThy.get_tthmss thy monos))
    1.20 -    (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy
    1.21 +    (Attribute.thms_of (PureThy.get_tthmss thy monos))
    1.22 +    (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
    1.23    end;
    1.24  
    1.25  end;