equal
deleted
inserted
replaced
2857 coind_wit_thms (map (pair []) ctor_witss) |
2857 coind_wit_thms (map (pair []) ctor_witss) |
2858 |> map (apsnd (map snd o minimize_wits)); |
2858 |> map (apsnd (map snd o minimize_wits)); |
2859 |
2859 |
2860 val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); |
2860 val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); |
2861 |
2861 |
2862 val policy = user_policy Derive_All_Facts_Note_Most; |
|
2863 |
|
2864 val (Jbnfs, lthy) = |
2862 val (Jbnfs, lthy) = |
2865 fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy => |
2863 fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy => |
2866 bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads) |
2864 bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) |
2867 (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy |
2865 (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy |
2868 |> register_bnf (Local_Theory.full_name lthy b)) |
2866 |> register_bnf (Local_Theory.full_name lthy b)) |
2869 tacss bs fs_maps setss_by_bnf Ts all_witss lthy; |
2867 tacss bs fs_maps setss_by_bnf Ts all_witss lthy; |
2870 |
2868 |
2871 val fold_maps = fold_thms lthy (map (fn bnf => |
2869 val fold_maps = fold_thms lthy (map (fn bnf => |