transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)

--- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Jul 23 13:10:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Jul 23 13:14:14 2013 +0200
@@ -430,7 +430,9 @@
   val merge = Symtab.merge eq_bnf;
 );
 
-val bnf_of = Symtab.lookup o Data.get o Context.Proof;
+fun bnf_of ctxt str =
+  Symtab.lookup (Data.get (Context.Proof ctxt)) str
+  |> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));