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