175 val (raw_full_dt_names', thy1) = |
175 val (raw_full_dt_names', thy1) = |
176 Datatype.add_datatype Datatype.default_config raw_full_dt_names raw_dts thy |
176 Datatype.add_datatype Datatype.default_config raw_full_dt_names raw_dts thy |
177 |
177 |
178 val lthy1 = Named_Target.theory_init thy1 |
178 val lthy1 = Named_Target.theory_init thy1 |
179 |
179 |
180 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) raw_full_dt_names' |
180 val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
181 val {descr, sorts, ...} = hd dtinfos |
181 val {descr, sorts, ...} = hd dtinfos |
182 |
182 |
183 val raw_tys = Datatype_Aux.get_rec_types descr sorts |
183 val raw_tys = Datatype_Aux.get_rec_types descr sorts |
184 val raw_ty_args = hd raw_tys |
184 val raw_ty_args = hd raw_tys |
185 |> snd o dest_Type |
185 |> snd o dest_Type |
192 val raw_distinct_thms = flat (map #distinct dtinfos) |
192 val raw_distinct_thms = flat (map #distinct dtinfos) |
193 val raw_induct_thm = #induct (hd dtinfos) |
193 val raw_induct_thm = #induct (hd dtinfos) |
194 val raw_induct_thms = #inducts (hd dtinfos) |
194 val raw_induct_thms = #inducts (hd dtinfos) |
195 val raw_exhaust_thms = map #exhaust dtinfos |
195 val raw_exhaust_thms = map #exhaust dtinfos |
196 val raw_size_trms = map HOLogic.size_const raw_tys |
196 val raw_size_trms = map HOLogic.size_const raw_tys |
197 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy1) (hd raw_full_dt_names') |
197 val raw_size_thms = Size.size_thms (Proof_Context.theory_of lthy1) (hd raw_full_dt_names') |
198 |> `(fn thms => (length thms) div 2) |
198 |> `(fn thms => (length thms) div 2) |
199 |> uncurry drop |
199 |> uncurry drop |
200 |
200 |
201 val raw_result = RawDtInfo |
201 val raw_result = RawDtInfo |
202 {raw_dt_names = raw_full_dt_names', |
202 {raw_dt_names = raw_full_dt_names', |
491 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
491 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
492 |
492 |
493 val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms |
493 val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms |
494 |
494 |
495 val (_, lthy9') = lthyC |
495 val (_, lthy9') = lthyC |
496 |> Local_Theory.declaration false (K (fold register_info infos)) |
496 |> Local_Theory.declaration {syntax = false, pervasive = false} (K (fold register_info infos)) |
497 |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) |
497 |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) |
498 ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') |
498 ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') |
499 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
499 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
500 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
500 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
501 ||>> Local_Theory.note ((thms_suffix "bn_inducts", []), qbn_inducts) |
501 ||>> Local_Theory.note ((thms_suffix "bn_inducts", []), qbn_inducts) |
683 let |
683 let |
684 val pre_typs = |
684 val pre_typs = |
685 map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs |
685 map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs |
686 |
686 |
687 (* this theory is used just for parsing *) |
687 (* this theory is used just for parsing *) |
688 val thy = ProofContext.theory_of lthy |
688 val thy = Proof_Context.theory_of lthy |
689 val tmp_thy = Theory.copy thy |
689 val tmp_thy = Theory.copy thy |
690 |
690 |
691 val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = |
691 val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = |
692 tmp_thy |
692 tmp_thy |
693 |> Sign.add_types_global pre_typs |
693 |> Sign.add_types_global pre_typs |