equal
deleted
inserted
replaced
400 |
400 |
401 val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; |
401 val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; |
402 |
402 |
403 val thy11 = thy10 |> |
403 val thy11 = thy10 |> |
404 Theory.add_path (space_implode "_" new_type_names) |> |
404 Theory.add_path (space_implode "_" new_type_names) |> |
405 PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |> |
405 PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |> |
406 put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> |
406 put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> |
407 Theory.parent_path; |
407 Theory.parent_path; |
408 |
408 |
409 val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11) |
409 val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11) |
410 addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms |
410 addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms |
457 |
457 |
458 val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; |
458 val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; |
459 |
459 |
460 val thy11 = thy10 |> |
460 val thy11 = thy10 |> |
461 Theory.add_path (space_implode "_" new_type_names) |> |
461 Theory.add_path (space_implode "_" new_type_names) |> |
462 PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |> |
462 PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |> |
463 put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> |
463 put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> |
464 Theory.parent_path; |
464 Theory.parent_path; |
465 |
465 |
466 val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11) |
466 val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11) |
467 addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms |
467 addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms |
548 |
548 |
549 val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; |
549 val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; |
550 |
550 |
551 val thy9 = thy8 |> |
551 val thy9 = thy8 |> |
552 Theory.add_path (space_implode "_" new_type_names) |> |
552 Theory.add_path (space_implode "_" new_type_names) |> |
553 PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |> |
553 PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |> |
554 put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> |
554 put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> |
555 Theory.parent_path; |
555 Theory.parent_path; |
556 |
556 |
557 val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9) |
557 val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9) |
558 addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms |
558 addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms |
570 size = size_thms, |
570 size = size_thms, |
571 simps = simps}) |
571 simps = simps}) |
572 end; |
572 end; |
573 |
573 |
574 val rep_datatype = gen_rep_datatype |
574 val rep_datatype = gen_rep_datatype |
575 (fn thy => map Attribute.thm_of o PureThy.get_tthmss thy) get_thm; |
575 (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm; |
576 val rep_datatype_i = gen_rep_datatype (K I) (K I); |
576 val rep_datatype_i = gen_rep_datatype (K I) (K I); |
577 |
577 |
578 (******************************** add datatype ********************************) |
578 (******************************** add datatype ********************************) |
579 |
579 |
580 fun gen_add_datatype prep_typ flat_names new_type_names dts thy = |
580 fun gen_add_datatype prep_typ flat_names new_type_names dts thy = |
582 val _ = Theory.requires thy "Datatype" "datatype definitions"; |
582 val _ = Theory.requires thy "Datatype" "datatype definitions"; |
583 |
583 |
584 (* this theory is used just for parsing *) |
584 (* this theory is used just for parsing *) |
585 |
585 |
586 val tmp_thy = thy |> |
586 val tmp_thy = thy |> |
587 Theory.prep_ext |> |
587 Theory.copy |> |
588 Theory.add_types (map (fn (tvs, tname, mx, _) => |
588 Theory.add_types (map (fn (tvs, tname, mx, _) => |
589 (tname, length tvs, mx)) dts); |
589 (tname, length tvs, mx)) dts); |
590 |
590 |
591 val sign = sign_of tmp_thy; |
591 val sign = sign_of tmp_thy; |
592 |
592 |