410 |
410 |
411 |
411 |
412 fun add_datatype (sdom, srec_tms, scon_ty_lists, |
412 fun add_datatype (sdom, srec_tms, scon_ty_lists, |
413 monos, type_intrs, type_elims) thy = |
413 monos, type_intrs, type_elims) thy = |
414 let val sign = sign_of thy |
414 let val sign = sign_of thy |
415 val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms |
415 val read_i = Sign.simple_read_term sign Ind_Syntax.iT |
|
416 val rec_tms = map read_i srec_tms |
416 val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists |
417 val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists |
417 val dom_sum = |
418 val dom_sum = |
418 if sdom = "" then |
419 if sdom = "" then |
419 Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") |
420 Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") |
420 (rec_tms, con_ty_lists) |
421 (rec_tms, con_ty_lists) |
421 else readtm sign Ind_Syntax.iT sdom |
422 else read_i sdom |
422 in |
423 in |
423 add_datatype_i (dom_sum, rec_tms, con_ty_lists, |
424 add_datatype_i (dom_sum, rec_tms, con_ty_lists, |
424 monos, type_intrs, type_elims) thy |
425 monos, type_intrs, type_elims) thy |
425 end |
426 end |
426 |
427 |