# HG changeset patch
# User blanchet
# Date 1406154240 -7200
# Node ID 231e90cf2892586ed131bffa76ad62067b4b2634
# Parent  959caab43a3d2c23df6da2d5106ac3c84e4f5ca1
use the noted theorems in 'BNF_Comp'

diff -r 959caab43a3d -r 231e90cf2892 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -878,9 +878,10 @@
 
     val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
       |> map (fn (b, def) => ((b, []), [([def], [])]))
-    val lthy'' = lthy' |> Local_Theory.notes notes |> snd
+
+    val (noted, lthy'') = lthy' |> Local_Theory.notes notes
   in
-    ((bnf'', (all_deads, absT_info)), lthy'')
+    ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
   end;
 
 exception BAD_DEAD of typ * typ;
diff -r 959caab43a3d -r 231e90cf2892 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -752,7 +752,6 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
-
     val bnf_map_def = Morphism.thm phi raw_map_def;
     val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
     val bnf_bd_def = Morphism.thm phi raw_bd_def;