equal
deleted
inserted
replaced
1670 |
1670 |
1671 fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN |
1671 fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN |
1672 mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); |
1672 mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); |
1673 |
1673 |
1674 val (Ibnfs, lthy) = |
1674 val (Ibnfs, lthy) = |
1675 fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy => |
1675 fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => |
1676 bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) |
1676 bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) |
1677 map_b rel_b set_bs consts lthy |
1677 map_b rel_b set_bs consts |
1678 |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy))) |
1678 #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy))) |
1679 bs tacss map_bs rel_bs set_bss |
1679 bs tacss map_bs rel_bs set_bss |
1680 ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) |
1680 ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) |
1681 lthy; |
1681 lthy; |
1682 |
1682 |
1683 val timer = time (timer "registered new datatypes as BNFs"); |
1683 val timer = time (timer "registered new datatypes as BNFs"); |