src/HOL/Tools/datatype_package.ML
changeset 5663 aad79a127628
parent 5661 6ecb6ea25f19
child 5720 ace664b0c978
equal deleted inserted replaced
5662:72a2e33d3b9e 5663:aad79a127628
   448 
   448 
   449     val thy11 = thy10 |>
   449     val thy11 = thy10 |>
   450       Theory.add_path (space_implode "_" new_type_names) |>
   450       Theory.add_path (space_implode "_" new_type_names) |>
   451       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   451       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   452       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   452       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   453       parent_path flat_names;
   453       Theory.parent_path;
   454 
   454 
   455     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   455     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   456       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   456       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   457       addIffs flat inject addDistinct (distinct, hd descr));
   457       addIffs flat inject addDistinct (distinct, hd descr));
   458 
   458