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

--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Aug 21 12:28:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Aug 21 13:48:25 2013 +0200
@@ -441,9 +441,9 @@
   val merge = Symtab.merge eq_bnf;
 );
 
-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))));
+fun bnf_of ctxt =
+  Symtab.lookup (Data.get (Context.Proof ctxt))
+  #> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
 
 
 

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 21 12:28:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 21 13:48:25 2013 +0200
@@ -140,7 +140,10 @@
   val merge = Symtab.merge eq_fp_sugar;
 );
 
-val fp_sugar_of = Symtab.lookup o Data.get o Context.Proof;
+fun fp_sugar_of ctxt =
+  Symtab.lookup (Data.get (Context.Proof ctxt))
+  #> Option.map (morph_fp_sugar
+    (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
 
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;