src/HOL/Tools/inductive_package.ML
changeset 5718 e5094d678285
parent 5662 72a2e33d3b9e
child 5891 92e0f5e6fd17
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Oct 21 17:48:02 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Oct 21 17:52:38 1998 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4         mk_cases:thm list -> string -> thm, mono:thm,
     1.5         unfold:thm}
     1.6    val add_inductive : bool -> bool -> string list -> string list
     1.7 -    -> thm list -> thm list -> theory -> theory *
     1.8 +    -> xstring list -> xstring list -> theory -> theory *
     1.9        {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
    1.10         intrs:thm list,
    1.11         mk_cases:thm list -> string -> thm, mono:thm,
    1.12 @@ -600,7 +600,8 @@
    1.13      val intr_ts'' = map subst intr_ts';
    1.14  
    1.15    in add_inductive_i verbose false "" coind false false cs'' intr_ts''
    1.16 -    monos con_defs thy
    1.17 +    (map (Attribute.thm_of) (PureThy.get_tthmss thy monos))
    1.18 +    (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy
    1.19    end;
    1.20  
    1.21  end;