1854 map2 (fn b => fn thms => |
1854 map2 (fn b => fn thms => |
1855 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1855 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1856 bs thmss) |
1856 bs thmss) |
1857 in |
1857 in |
1858 timer; |
1858 timer; |
1859 ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs, |
1859 ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, |
1860 co_induct = ctor_induct_thm, strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1860 xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, |
|
1861 xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1861 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms, |
1862 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms, |
1862 set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, un_fold_thms = ctor_fold_thms, |
1863 set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, |
1863 co_rec_thms = ctor_rec_thms}, |
1864 xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms}, |
1864 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
1865 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
1865 end; |
1866 end; |
1866 |
1867 |
1867 val _ = |
1868 val _ = |
1868 Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" |
1869 Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" |