# HG changeset patch
# User traytel
# Date 1374578054 -7200
# Node ID 6bafe21b13b28ffd7d4d6823b998d89742d937b6
# Parent  fdc04f9bf906bd67fea35caff21115bd419705ec
transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)

diff -r fdc04f9bf906 -r 6bafe21b13b2 src/HOL/BNF/Tools/bnf_def.ML
--- 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))));