keep the qualification of bindings when noting bnf theorems

--- 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