use the noted theorems in 'BNF_Comp'
authorblanchet
Thu Jul 24 00:24:00 2014 +0200 (2014-07-24)
changeset 57632231e90cf2892
parent 57631 959caab43a3d
child 57633 4ff8c090d580
use the noted theorems in 'BNF_Comp'
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -878,9 +878,10 @@
     1.4  
     1.5      val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
     1.6        |> map (fn (b, def) => ((b, []), [([def], [])]))
     1.7 -    val lthy'' = lthy' |> Local_Theory.notes notes |> snd
     1.8 +
     1.9 +    val (noted, lthy'') = lthy' |> Local_Theory.notes notes
    1.10    in
    1.11 -    ((bnf'', (all_deads, absT_info)), lthy'')
    1.12 +    ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'')
    1.13    end;
    1.14  
    1.15  exception BAD_DEAD of typ * typ;
     2.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 00:24:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -752,7 +752,6 @@
     2.4  
     2.5      val phi = Proof_Context.export_morphism lthy_old lthy;
     2.6  
     2.7 -
     2.8      val bnf_map_def = Morphism.thm phi raw_map_def;
     2.9      val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
    2.10      val bnf_bd_def = Morphism.thm phi raw_bd_def;