equal
deleted
inserted
replaced
65 raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy = |
65 raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy = |
66 let |
66 let |
67 val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions"; |
67 val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions"; |
68 val ctxt = ProofContext.init thy; |
68 val ctxt = ProofContext.init thy; |
69 |
69 |
70 val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs; |
70 val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs; |
71 val (intr_names, intr_tms) = split_list (map fst intr_specs); |
71 val (intr_names, intr_tms) = split_list (map fst intr_specs); |
72 val case_names = RuleCases.case_names intr_names; |
72 val case_names = RuleCases.case_names intr_names; |
73 |
73 |
74 (*recT and rec_params should agree for all mutually recursive components*) |
74 (*recT and rec_params should agree for all mutually recursive components*) |
75 val rec_hds = map head_of rec_tms; |
75 val rec_hds = map head_of rec_tms; |