equal
deleted
inserted
replaced
2430 |
2430 |
2431 fun wit_tac thms ctxt = |
2431 fun wit_tac thms ctxt = |
2432 mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; |
2432 mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; |
2433 |
2433 |
2434 val (Jbnfs, lthy) = |
2434 val (Jbnfs, lthy) = |
2435 fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => |
2435 fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => |
2436 fn consts => |
2436 fn consts => |
2437 bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) |
2437 bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) |
2438 (SOME deads) map_b rel_b set_bs consts) |
2438 (SOME deads) map_b rel_b set_bs consts) |
2439 bs tacss map_bs rel_bs set_bss wit_thmss |
2439 tacss map_bs rel_bs set_bss wit_thmss |
2440 ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ |
2440 ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ |
2441 all_witss) ~~ map SOME Jrels) |
2441 all_witss) ~~ map SOME Jrels) |
2442 lthy; |
2442 lthy; |
2443 |
2443 |
2444 val timer = time (timer "registered new codatatypes as BNFs"); |
2444 val timer = time (timer "registered new codatatypes as BNFs"); |