# HG changeset patch # User traytel # Date 1380747559 -7200 # Node ID 369a4a14583a2e6645fbd54c55659d405deecb6b # Parent c931190b8c5c35e0dbbdfad1313221b4ff7ad1d9 keep the qualification of bindings when noting bnf theorems diff -r c931190b8c5c -r 369a4a14583a src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Wed Oct 02 19:49:31 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Oct 02 22:59:19 2013 +0200 @@ -539,11 +539,14 @@ val smart_max_inline_size = 25; (*FUDGE*) -fun note_bnf_thms fact_policy qualify bnf_b bnf = +fun note_bnf_thms fact_policy qualify' bnf_b bnf = let val axioms = axioms_of_bnf bnf; val facts = facts_of_bnf bnf; val wits = wits_of_bnf bnf; + val qualify = + let val (_, qs, _) = Binding.dest bnf_b; + in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify' end; in (if fact_policy = Note_All then let