# HG changeset patch
# User wenzelm
# Date 1407934623 -7200
# Node ID f4ff42c5b05b5e36d151c012c3305789ae3526c5
# Parent  f14c1248d06432f55675029298205cea1fff63db
transfer result of Global_Theory.add_thms_dynamic to context stack;
more accurate local aliases;

diff -r f14c1248d064 -r f4ff42c5b05b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 13 13:57:55 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 13 14:57:03 2014 +0200
@@ -50,6 +50,7 @@
   val markup_const: Proof.context -> string -> string
   val pretty_const: Proof.context -> string -> Pretty.T
   val transfer: theory -> Proof.context -> Proof.context
+  val transfer_facts: theory -> Proof.context -> Proof.context
   val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val facts_of: Proof.context -> Facts.T
@@ -323,16 +324,19 @@
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
-      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
+      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
       if Consts.eq_consts (thy_consts, global_consts) then consts
-      else (Consts.merge (local_consts, thy_consts), thy_consts)
+      else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
     end);
 
 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
 
+fun transfer_facts thy =
+  map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts));
+
 fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
 
 fun background_theory_result f ctxt =
diff -r f14c1248d064 -r f4ff42c5b05b src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Wed Aug 13 13:57:55 2014 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Wed Aug 13 14:57:03 2014 +0200
@@ -68,19 +68,17 @@
       |> Local_Theory.background_theory
         (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
          Context.theory_map (new_entry name))
-      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
+      |> Local_Theory.map_contexts (fn _ => fn ctxt =>
+          ctxt
+          |> Context.proof_map (new_entry name)
+          |> Proof_Context.transfer_facts (Proof_Context.theory_of ctxt))
       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
-      |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
-          let
-            val binding' = Morphism.binding phi binding;
-            val context' =
-              context |> Context.mapping
-                (Global_Theory.alias_fact binding' name)
-                (fn ctxt =>
-                  if Facts.defined (Proof_Context.facts_of ctxt) name
-                  then Proof_Context.fact_alias binding' name ctxt
-                  else ctxt);
-          in context' end);
+      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
+          let val binding' = Morphism.binding phi binding in
+            Context.mapping
+              (Global_Theory.alias_fact binding' name)
+              (Proof_Context.fact_alias binding' name)
+          end);
   in (name, lthy') end;
 
 val _ =