617 val qs = Binding.path_of base_b; |
617 val qs = Binding.path_of base_b; |
618 val n = Binding.name_of base_b; |
618 val n = Binding.name_of base_b; |
619 in |
619 in |
620 Binding.prefix_name rawN |
620 Binding.prefix_name rawN |
621 #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
621 #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
622 #> Binding.conceal |
622 #> Binding.concealed |
623 end; |
623 end; |
624 |
624 |
625 val ((bnfs, (deadss, livess)), accum) = |
625 val ((bnfs, (deadss, livess)), accum) = |
626 apfst (apsnd split_list o split_list) |
626 apfst (apsnd split_list o split_list) |
627 (@{fold_map 2} |
627 (@{fold_map 2} |
628 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs |
628 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs |
629 ((empty_comp_cache, empty_unfolds), lthy)); |
629 ((empty_comp_cache, empty_unfolds), lthy)); |
630 |
630 |
631 fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) |
631 fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) |
632 #> Binding.conceal; |
632 #> Binding.concealed; |
633 |
633 |
634 val Ass = map (map dest_TFree) livess; |
634 val Ass = map (map dest_TFree) livess; |
635 val Ds' = fold (fold Term.add_tfreesT) deadss []; |
635 val Ds' = fold (fold Term.add_tfreesT) deadss []; |
636 val Ds = union (op =) Ds' Ds0; |
636 val Ds = union (op =) Ds' Ds0; |
637 val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass); |
637 val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass); |
644 normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum; |
644 normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum; |
645 |
645 |
646 val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; |
646 val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; |
647 |
647 |
648 fun pre_qualify b = Binding.qualify false (Binding.name_of b) |
648 fun pre_qualify b = Binding.qualify false (Binding.name_of b) |
649 #> not (Config.get lthy' bnf_note_all) ? Binding.conceal; |
649 #> not (Config.get lthy' bnf_note_all) ? Binding.concealed; |
650 |
650 |
651 val ((pre_bnfs, (deadss, absT_infos)), lthy'') = |
651 val ((pre_bnfs, (deadss, absT_infos)), lthy'') = |
652 @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) |
652 @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) |
653 bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy' |
653 bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy' |
654 |>> split_list |
654 |>> split_list |