src/HOL/Tools/inductive_package.ML
changeset 6092 d9db67970c73
parent 5891 92e0f5e6fd17
child 6141 a6922171b396
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 12 13:40:08 1999 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 12 13:54:51 1999 +0100
     1.3 @@ -464,12 +464,11 @@
     1.4        else standard (raw_induct RSN (2, rev_mp));
     1.5  
     1.6      val thy'' = thy' |>
     1.7 -      PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
     1.8 -      (if no_elim then I else PureThy.add_tthmss
     1.9 -        [(("elims", Attribute.tthms_of elims), [])]) |>
    1.10 -      (if no_ind then I else PureThy.add_tthms
    1.11 -        [(((if coind then "co" else "") ^ "induct",
    1.12 -          Attribute.tthm_of induct), [])]) |>
    1.13 +      PureThy.add_thmss [(("intrs", intrs), [])] |>
    1.14 +      (if no_elim then I else PureThy.add_thmss
    1.15 +        [(("elims", elims), [])]) |>
    1.16 +      (if no_ind then I else PureThy.add_thms
    1.17 +        [(((if coind then "co" else "") ^ "induct", induct), [])]) |>
    1.18        Theory.parent_path;
    1.19  
    1.20    in (thy'',
    1.21 @@ -517,7 +516,7 @@
    1.22  
    1.23      val thy'' = thy' |>
    1.24        (if coind then I
    1.25 -       else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
    1.26 +       else PureThy.add_thms [(("induct", induct), [])]) |>
    1.27        Theory.parent_path
    1.28  
    1.29    in (thy'',
    1.30 @@ -600,8 +599,8 @@
    1.31      val intr_ts'' = map subst intr_ts';
    1.32  
    1.33    in add_inductive_i verbose false "" coind false false cs'' intr_ts''
    1.34 -    (Attribute.thms_of (PureThy.get_tthmss thy monos))
    1.35 -    (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
    1.36 +    (PureThy.get_thmss thy monos)
    1.37 +    (PureThy.get_thmss thy con_defs) thy
    1.38    end;
    1.39  
    1.40  end;