just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
more thorough background_notes: distribute global notes to all contexts;

--- a/src/HOL/Lattices_Big.thy	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/HOL/Lattices_Big.thy	Fri Mar 14 10:08:36 2014 +0100
@@ -640,6 +640,11 @@
   shows "Max M \<le> Max N"
   using assms by (fact Max.antimono)
 
+end
+
+context linorder  (* FIXME *)
+begin
+
 lemma mono_Min_commute:
   assumes "mono f"
   assumes "finite A" and "A \<noteq> {}"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -459,7 +459,7 @@
       else
         is_too_complex
     val local_facts = Proof_Context.facts_of ctxt
-    val named_locals = local_facts |> Facts.dest_static []
+    val named_locals = local_facts |> Facts.dest_static [global_facts]
     val assms = Assumption.all_assms_of ctxt
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso
@@ -467,14 +467,12 @@
     val unnamed_locals =
       union Thm.eq_thm_prop (Facts.props local_facts) chained
       |> filter is_good_unnamed_local |> map (pair "" o single)
-    val full_space =
-      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
-    fun add_facts global foldx facts =
+    fun add_facts global foldx =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
-           (Facts.is_concealed facts name0 orelse
+           (Facts.is_concealed local_facts name0 orelse
             (not generous andalso is_blacklisted_or_something name0)) then
           accum
         else
@@ -499,8 +497,7 @@
                            if name0 = "" then
                              backquote_thm ctxt th
                            else
-                             [Facts.extern ctxt facts name0,
-                              Name_Space.extern ctxt full_space name0]
+                             [Facts.extern ctxt local_facts name0]
                              |> find_first check_thms
                              |> the_default name0
                              |> make_name reserved multi j),
@@ -515,8 +512,8 @@
     (* The single-theorem names go before the multiple-theorem ones (e.g.,
        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
        available. *)
-    `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
-          |> add_facts true Facts.fold_static global_facts global_facts
+    `I [] |> add_facts false fold (unnamed_locals @ named_locals)
+          |> add_facts true Facts.fold_static global_facts
           |> op @
   end
 

--- a/src/Pure/Isar/attrib.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -213,7 +213,7 @@
 
 fun gen_thm pick = Scan.depend (fn context =>
   let
-    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
+    val get = Proof_Context.get_fact_generic context;
     val get_fact = get o Facts.Fact;
     fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   in
@@ -249,6 +249,8 @@
 
 (** partial evaluation -- observing rule/declaration/mixed attributes **)
 
+(*NB: result length may change due to rearrangement of symbolic expression*)
+
 local
 
 fun apply_att src (context, th) =

--- a/src/Pure/Isar/generic_target.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/generic_target.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -179,8 +179,7 @@
   end;
 
 fun locale_notes locale kind global_facts local_facts =
-  Local_Theory.background_theory
-    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
+  Local_Theory.background_notes kind (Attrib.map_facts (K []) global_facts) #>
   (fn lthy => lthy |>
     Local_Theory.target (fn ctxt => ctxt |>
       Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
@@ -311,7 +310,7 @@
     |> pair (lhs, def));
 
 fun theory_notes kind global_facts local_facts =
-  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
+  Local_Theory.background_notes kind global_facts #>
   (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
     if level = Local_Theory.level lthy then ctxt
     else

--- a/src/Pure/Isar/local_theory.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -32,6 +32,8 @@
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
+  val background_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+    local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
@@ -215,6 +217,19 @@
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
+fun background_notes kind facts lthy =
+  let
+    val facts1 = Attrib.partial_evaluation lthy facts;
+    val facts0 = Attrib.map_facts (K []) facts1;
+  in
+    lthy
+    |> background_theory (Attrib.global_notes kind facts1 #> snd)
+    |> map_contexts (fn _ => fn ctxt => ctxt
+      |> Proof_Context.map_naming (K (naming_of lthy))
+      |> Attrib.local_notes kind facts0 |> snd
+      |> Proof_Context.restore_naming ctxt)
+  end;
+
 
 (* target contexts *)
 

--- a/src/Pure/Isar/locale.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -561,7 +561,7 @@
           (* Registrations *)
           (fn thy =>
             fold_rev (fn (_, morph) =>
-              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
+              snd o Attrib.global_notes kind (Element.transform_facts morph facts))  (* FIXME background_notes *)
             (registrations_of (Context.Theory thy) loc) thy));
 
 

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -53,9 +53,7 @@
   val transfer: 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 extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
-  val markup_fact: Proof.context -> string -> Markup.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
   val read_class: Proof.context -> string -> class
@@ -120,6 +118,7 @@
     (term list list * (Proof.context -> Proof.context)) * Proof.context
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
+  val get_fact_generic: Context.generic -> Facts.ref -> thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
@@ -209,7 +208,7 @@
     syntax: Local_Syntax.T,      (*local syntax*)
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
-    facts: Facts.T,              (*local facts*)
+    facts: Facts.T,              (*cumulative facts*)
     cases: cases};               (*named case contexts: case, is_proper, running index*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
@@ -223,7 +222,7 @@
       Local_Syntax.init thy,
       (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
       (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
-      Facts.empty,
+      Global_Theory.facts_of thy,
       empty_cases);
 );
 
@@ -340,28 +339,10 @@
 
 (** pretty printing **)
 
-(* extern *)
-
-fun which_facts ctxt name =
-  let
-    val local_facts = facts_of ctxt;
-    val global_facts = Global_Theory.facts_of (theory_of ctxt);
-  in
-    if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
-    then local_facts else global_facts
-  end;
-
-fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name;
-
-fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
-
-
-(* pretty *)
-
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
-  Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
+  Pretty.block [Pretty.mark_str (Facts.markup_extern ctxt (facts_of ctxt) a), Pretty.str ":"];
 
 fun pretty_fact ctxt =
   let
@@ -911,12 +892,13 @@
 end;
 
 
-(* get_thm(s) *)
+(* get facts *)
 
 local
 
-fun retrieve_thms pick ctxt (Facts.Fact s) =
+fun retrieve_thms pick context (Facts.Fact s) =
       let
+        val ctxt = Context.the_proof context;
         val pos = Syntax.read_token_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
@@ -927,34 +909,28 @@
         fun prove_fact th =
           Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
         val results = map_filter (try prove_fact) (potential_facts ctxt prop');
-        val res =
+        val thm =
           (case distinct Thm.eq_thm_prop results of
-            [res] => res
+            [thm] => thm
           | [] => err "Failed to retrieve literal fact"
           | _ => err "Ambiguous specification of literal fact");
-      in pick ("", Position.none) [res] end
-  | retrieve_thms pick ctxt xthmref =
+      in pick ("", Position.none) [thm] end
+  | retrieve_thms pick context (Facts.Named ((xname, pos), ivs)) =
       let
-        val thy = theory_of ctxt;
-        val local_facts = facts_of ctxt;
-        val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
-        val name = Facts.name_of_ref thmref;
-        val pos = Facts.pos_of_ref xthmref;
-        val thms =
-          if name = "" then [Thm.transfer thy Drule.dummy_thm]
-          else
-            (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME (_, ths) =>
-                (Context_Position.report ctxt pos
-                  (Name_Space.markup (Facts.space_of local_facts) name);
-                 map (Thm.transfer thy) (Facts.select thmref ths))
-            | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
-      in pick (name, pos) thms end;
+        val thy = Context.theory_of context;
+        val facts = Context.cases Global_Theory.facts_of facts_of context;
+        val (name, thms) =
+          (case xname of
+            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
+          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
+          | _ => Facts.retrieve context facts (xname, pos));
+      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
 
 in
 
-val get_fact = retrieve_thms (K I);
-val get_fact_single = retrieve_thms Facts.the_single;
+val get_fact_generic = retrieve_thms (K I);
+val get_fact = retrieve_thms (K I) o Context.Proof;
+val get_fact_single = retrieve_thms Facts.the_single o Context.Proof;
 
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;

--- a/src/Pure/Tools/find_theorems.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -381,14 +381,11 @@
 
 fun all_facts_of ctxt =
   let
-    fun visible_facts facts =
+    val facts = Proof_Context.facts_of ctxt
+    val visible_facts =
       Facts.dest_static [] facts
       |> filter_out (Facts.is_concealed facts o #1);
-  in
-    maps Facts.selections
-     (visible_facts (Proof_Context.facts_of ctxt) @
-      visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)))
-  end;
+  in maps Facts.selections visible_facts end;
 
 fun filter_theorems ctxt theorems query =
   let
@@ -453,9 +450,10 @@
       (case thmref of
         Facts.Named ((name, _), sel) => (name, sel)
       | Facts.Fact _ => raise Fail "Illegal literal fact");
+    val (markup, _) = Facts.markup_extern ctxt (Proof_Context.facts_of ctxt) name;
   in
-    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
-      Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
+    [Pretty.mark_str (markup, name), Pretty.str (Facts.string_of_selection sel),
+      Pretty.str ":", Pretty.brk 1]
   end;
 
 in

--- a/src/Pure/facts.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/facts.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -26,7 +26,9 @@
   val check: Context.generic -> T -> xstring * Position.T -> string
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
+  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
+  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: T list -> T -> (string * thm list) list
@@ -155,6 +157,7 @@
 
 val intern = Name_Space.intern o space_of;
 fun extern ctxt = Name_Space.extern ctxt o space_of;
+fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
 
 val defined = is_some oo (Name_Space.lookup_key o facts_of);
 
@@ -164,6 +167,18 @@
   | SOME (_, Static ths) => SOME (true, ths)
   | SOME (_, Dynamic f) => SOME (false, f context));
 
+fun retrieve context facts (xname, pos) =
+  let
+    val name = check context facts (xname, pos);
+    val thms =
+      (case lookup context facts name of
+        SOME (static, thms) =>
+          (if static then ()
+           else Context_Position.report_generic context pos (Markup.dynamic_fact name);
+           thms)
+      | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
+  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+
 fun fold_static f =
   Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
 

--- a/src/Pure/global_theory.ML	Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/global_theory.ML	Fri Mar 14 10:08:36 2014 +0100
@@ -11,7 +11,6 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val all_thms_of: theory -> (string * thm) list
@@ -64,31 +63,13 @@
 fun hide_fact fully name = Data.map (Facts.hide fully name);
 
 
-(** retrieve theorems **)
-
-fun get_fact context thy xthmref =
-  let
-    val facts = facts_of thy;
-    val xname = Facts.name_of_ref xthmref;
-    val pos = Facts.pos_of_ref xthmref;
+(* retrieve theorems *)
 
-    val name =
-      (case intern_fact thy xname of
-        "_" => "Pure.asm_rl"
-      | name => name);
-    val res = Facts.lookup context facts name;
-  in
-    (case res of
-      NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
-    | SOME (static, ths) =>
-        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
-         if static then ()
-         else Context_Position.report_generic context pos (Markup.dynamic_fact name);
-         Facts.select xthmref (map (Thm.transfer thy) ths)))
-  end;
+fun get_thms thy xname =
+  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
 
-fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
-fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
+fun get_thm thy xname =
+  Facts.the_single (xname, Position.none) (get_thms thy xname);
 
 fun all_thms_of thy =
   Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];