equal
deleted
inserted
replaced
1728 |
1728 |
1729 fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN |
1729 fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN |
1730 mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); |
1730 mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); |
1731 |
1731 |
1732 val (Ibnfs, lthy) = |
1732 val (Ibnfs, lthy) = |
1733 fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy => |
1733 fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy => |
1734 bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) |
1734 bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) |
1735 map_b rel_b set_bs consts lthy |
1735 map_b rel_b set_bs consts lthy |
1736 |> register_bnf (Local_Theory.full_name lthy b)) |
1736 |> register_bnf (Local_Theory.full_name lthy b)) |
1737 tacss map_bs rel_bs set_bss |
1737 bs tacss map_bs rel_bs set_bss |
1738 ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) |
1738 ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) |
1739 lthy; |
1739 lthy; |
1740 |
1740 |
1741 val timer = time (timer "registered new datatypes as BNFs"); |
1741 val timer = time (timer "registered new datatypes as BNFs"); |
1742 |
1742 |