transfer result of Global_Theory.add_thms_dynamic to context stack;
authorwenzelm
Wed Aug 13 14:57:03 2014 +0200 (2014-08-13)
changeset 57928f4ff42c5b05b
parent 57927 f14c1248d064
child 57929 c5063c033a5a
transfer result of Global_Theory.add_thms_dynamic to context stack;
more accurate local aliases;
src/Pure/Isar/proof_context.ML
src/Pure/Tools/named_theorems.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 13 13:57:55 2014 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 13 14:57:03 2014 +0200
     1.3 @@ -50,6 +50,7 @@
     1.4    val markup_const: Proof.context -> string -> string
     1.5    val pretty_const: Proof.context -> string -> Pretty.T
     1.6    val transfer: theory -> Proof.context -> Proof.context
     1.7 +  val transfer_facts: theory -> Proof.context -> Proof.context
     1.8    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
     1.9    val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    1.10    val facts_of: Proof.context -> Facts.T
    1.11 @@ -323,16 +324,19 @@
    1.12    map_tsig (fn tsig as (local_tsig, global_tsig) =>
    1.13      let val thy_tsig = Sign.tsig_of thy in
    1.14        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
    1.15 -      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
    1.16 +      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
    1.17      end) |>
    1.18    map_consts (fn consts as (local_consts, global_consts) =>
    1.19      let val thy_consts = Sign.consts_of thy in
    1.20        if Consts.eq_consts (thy_consts, global_consts) then consts
    1.21 -      else (Consts.merge (local_consts, thy_consts), thy_consts)
    1.22 +      else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
    1.23      end);
    1.24  
    1.25  fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
    1.26  
    1.27 +fun transfer_facts thy =
    1.28 +  map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts));
    1.29 +
    1.30  fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
    1.31  
    1.32  fun background_theory_result f ctxt =
     2.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Aug 13 13:57:55 2014 +0200
     2.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Aug 13 14:57:03 2014 +0200
     2.3 @@ -68,19 +68,17 @@
     2.4        |> Local_Theory.background_theory
     2.5          (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
     2.6           Context.theory_map (new_entry name))
     2.7 -      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
     2.8 +      |> Local_Theory.map_contexts (fn _ => fn ctxt =>
     2.9 +          ctxt
    2.10 +          |> Context.proof_map (new_entry name)
    2.11 +          |> Proof_Context.transfer_facts (Proof_Context.theory_of ctxt))
    2.12        |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
    2.13 -      |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
    2.14 -          let
    2.15 -            val binding' = Morphism.binding phi binding;
    2.16 -            val context' =
    2.17 -              context |> Context.mapping
    2.18 -                (Global_Theory.alias_fact binding' name)
    2.19 -                (fn ctxt =>
    2.20 -                  if Facts.defined (Proof_Context.facts_of ctxt) name
    2.21 -                  then Proof_Context.fact_alias binding' name ctxt
    2.22 -                  else ctxt);
    2.23 -          in context' end);
    2.24 +      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
    2.25 +          let val binding' = Morphism.binding phi binding in
    2.26 +            Context.mapping
    2.27 +              (Global_Theory.alias_fact binding' name)
    2.28 +              (Proof_Context.fact_alias binding' name)
    2.29 +          end);
    2.30    in (name, lthy') end;
    2.31  
    2.32  val _ =