--- 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;