equal
deleted
inserted
replaced
582 Binding.prefix_name rawN |
582 Binding.prefix_name rawN |
583 #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
583 #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
584 #> Binding.conceal |
584 #> Binding.conceal |
585 end; |
585 end; |
586 |
586 |
587 val ((bnfs, (deadss, livess)), ((_, unfold_set), lthy)) = |
587 val ((bnfs, (deadss, livess)), accum) = |
588 apfst (apsnd split_list o split_list) |
588 apfst (apsnd split_list o split_list) |
589 (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs |
589 (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs |
590 ((empty_comp_cache, empty_unfolds), lthy)); |
590 ((empty_comp_cache, empty_unfolds), lthy)); |
591 |
591 |
592 fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) |
592 fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) |
596 val resDs = fold (subtract (op =)) Ass resBs; |
596 val resDs = fold (subtract (op =)) Ass resBs; |
597 val Ds = fold (fold Term.add_tfreesT) deadss Ds0; |
597 val Ds = fold (fold Term.add_tfreesT) deadss Ds0; |
598 |
598 |
599 val timer = time (timer "Construction of BNFs"); |
599 val timer = time (timer "Construction of BNFs"); |
600 |
600 |
601 val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = |
601 val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) = |
602 normalize_bnfs norm_qualify Ass Ds fp_sort bnfs unfold_set lthy; |
602 normalize_bnfs norm_qualify Ass Ds fp_sort bnfs accum; |
603 |
603 |
604 val Dss = map3 (append oo map o nth) livess kill_poss deadss; |
604 val Dss = map3 (append oo map o nth) livess kill_poss deadss; |
605 |
605 |
606 fun pre_qualify b = Binding.qualify false (Binding.name_of b) |
606 fun pre_qualify b = Binding.qualify false (Binding.name_of b) |
607 #> Config.get lthy' bnf_note_all = false ? Binding.conceal; |
607 #> Config.get lthy' bnf_note_all = false ? Binding.conceal; |