equal
deleted
inserted
replaced
2853 |> map (apsnd (map snd o minimize_wits)); |
2853 |> map (apsnd (map snd o minimize_wits)); |
2854 |
2854 |
2855 val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); |
2855 val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); |
2856 |
2856 |
2857 val (Jbnfs, lthy) = |
2857 val (Jbnfs, lthy) = |
2858 fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => |
2858 fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy => |
2859 bnf_def Dont_Inline user_policy I tacs (wit_tac thms) (SOME deads) |
2859 bnf_def Dont_Inline user_policy I tacs (wit_tac thms) (SOME deads) |
2860 ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) |
2860 ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy |
|
2861 |> register_bnf (Local_Theory.full_name lthy b)) |
2861 tacss bs fs_maps setss_by_bnf Ts all_witss lthy; |
2862 tacss bs fs_maps setss_by_bnf Ts all_witss lthy; |
2862 |
2863 |
2863 val fold_maps = Local_Defs.fold lthy (map (fn bnf => |
2864 val fold_maps = Local_Defs.fold lthy (map (fn bnf => |
2864 mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs); |
2865 mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs); |
2865 |
2866 |