equal
deleted
inserted
replaced
537 |
537 |
538 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; |
538 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; |
539 |
539 |
540 val smart_max_inline_size = 25; (*FUDGE*) |
540 val smart_max_inline_size = 25; (*FUDGE*) |
541 |
541 |
542 fun note_bnf_thms fact_policy qualify bnf_b bnf = |
542 fun note_bnf_thms fact_policy qualify' bnf_b bnf = |
543 let |
543 let |
544 val axioms = axioms_of_bnf bnf; |
544 val axioms = axioms_of_bnf bnf; |
545 val facts = facts_of_bnf bnf; |
545 val facts = facts_of_bnf bnf; |
546 val wits = wits_of_bnf bnf; |
546 val wits = wits_of_bnf bnf; |
|
547 val qualify = |
|
548 let val (_, qs, _) = Binding.dest bnf_b; |
|
549 in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify' end; |
547 in |
550 in |
548 (if fact_policy = Note_All then |
551 (if fact_policy = Note_All then |
549 let |
552 let |
550 val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); |
553 val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); |
551 val notes = |
554 val notes = |