363 let |
363 let |
364 val n = length (HOLogic.dest_concls (Thm.concl_of induction)); |
364 val n = length (HOLogic.dest_concls (Thm.concl_of induction)); |
365 fun proj i = ProjectRule.project induction (i + 1); |
365 fun proj i = ProjectRule.project induction (i + 1); |
366 |
366 |
367 fun named_rules (name, {index, exhaustion, ...}: datatype_info) = |
367 fun named_rules (name, {index, exhaustion, ...}: datatype_info) = |
368 [(("", proj index), [InductAttrib.induct_type_global name]), |
368 [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]), |
369 (("", exhaustion), [InductAttrib.cases_type_global name])]; |
369 (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])]; |
370 fun unnamed_rule i = |
370 fun unnamed_rule i = |
371 (("", proj i), [Drule.kind_internal, InductAttrib.induct_type_global ""]); |
371 (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]); |
372 in |
372 in |
373 PureThy.add_thms |
373 PureThy.add_thms |
374 (List.concat (map named_rules infos) @ |
374 (List.concat (map named_rules infos) @ |
375 map unnamed_rule (length infos upto n - 1)) #> snd #> |
375 map unnamed_rule (length infos upto n - 1)) #> snd #> |
376 PureThy.add_thmss [(("inducts", |
376 PureThy.add_thmss [(("inducts", |