# HG changeset patch
# User traytel
# Date 1377085705 -7200
# Node ID f4d2c64c7aa8d50c9732bf58e2bd4ef08c08d383
# Parent  f4c6f8f6515b2faf650c43a6f835af7f42e97262
transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)

diff -r f4c6f8f6515b -r f4d2c64c7aa8 src/HOL/BNF/Tools/bnf_def.ML
--- 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))));
 
 
 
diff -r f4c6f8f6515b -r f4d2c64c7aa8 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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;