find dynamic facts as well, but static ones are preferred;
tuned;

--- a/src/Pure/Isar/proof_context.ML	Tue May 10 15:48:37 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue May 10 22:25:06 2016 +0200
@@ -63,7 +63,7 @@
   val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val facts_of: Proof.context -> Facts.T
   val facts_of_fact: Proof.context -> string -> Facts.T
-  val markup_extern_fact: Proof.context -> string -> Markup.T * xstring
+  val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
@@ -410,7 +410,13 @@
   end;
 
 fun markup_extern_fact ctxt name =
-  Facts.markup_extern ctxt (facts_of_fact ctxt name) name;
+  let
+    val facts = facts_of_fact ctxt name;
+    val (markup, xname) = Facts.markup_extern ctxt facts name;
+    val markups =
+      if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name]
+      else [markup];
+  in (markups, xname) end;
 
 
 
@@ -419,7 +425,7 @@
 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_extern_fact ctxt a), Pretty.str ":"];
+  Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"];
 
 fun pretty_fact ctxt =
   let

--- a/src/Pure/Tools/find_theorems.ML	Tue May 10 15:48:37 2016 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue May 10 22:25:06 2016 +0200
@@ -335,10 +335,12 @@
 val qual_ord = int_ord o apply2 Long_Name.qualification;
 val txt_ord = int_ord o apply2 size;
 
-fun nicer_name (x, i) (y, j) =
-  (case hidden_ord (x, y) of EQUAL =>
-    (case index_ord (i, j) of EQUAL =>
-      (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
+fun nicer_name ((a, x), i) ((b, y), j) =
+  (case bool_ord (a, b) of EQUAL =>
+    (case hidden_ord (x, y) of EQUAL =>
+      (case index_ord (i, j) of EQUAL =>
+        (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
+      | ord => ord)
     | ord => ord)
   | ord => ord) <> GREATER;
 
@@ -357,8 +359,10 @@
 fun nicer_shortest ctxt =
   let
     fun extern_shortest name =
-      Name_Space.extern_shortest ctxt
-        (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
+      let
+        val facts = Proof_Context.facts_of_fact ctxt name;
+        val space = Facts.space_of facts;
+      in (Facts.is_dynamic facts name, Name_Space.extern_shortest ctxt space name) end;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (extern_shortest x, i) (extern_shortest y, j)
@@ -389,8 +393,8 @@
     val local_facts = Proof_Context.facts_of ctxt;
     val global_facts = Global_Theory.facts_of thy;
   in
-   (Facts.dest_static false [global_facts] local_facts @
-     Facts.dest_static false [] global_facts)
+   (Facts.dest_all (Context.Proof ctxt) false [global_facts] local_facts @
+     Facts.dest_all (Context.Proof ctxt) false [] global_facts)
    |> maps Facts.selections
    |> map (apsnd transfer)
   end;
@@ -459,7 +463,7 @@
         Facts.Named ((name, _), sel) => (name, sel)
       | Facts.Fact _ => raise Fail "Illegal literal fact");
   in
-    [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
+    [Pretty.marks_str (#1 (Proof_Context.markup_extern_fact ctxt name), name),
       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   end;
 

--- a/src/Pure/facts.ML	Tue May 10 15:48:37 2016 +0200
+++ b/src/Pure/facts.ML	Tue May 10 22:25:06 2016 +0200
@@ -28,12 +28,14 @@
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
+  val defined: T -> string -> bool
+  val is_dynamic: T -> string -> bool
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
   val retrieve: Context.generic -> T -> xstring * Position.T ->
     {name: string, static: bool, thms: thm list}
-  val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: bool -> T list -> T -> (string * thm list) list
+  val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
@@ -168,6 +170,11 @@
 
 val defined = Name_Space.defined o facts_of;
 
+fun is_dynamic facts name =
+  (case Name_Space.lookup (facts_of facts) name of
+    SOME (Dynamic _) => true
+  | _ => false);
+
 fun lookup context facts name =
   (case Name_Space.lookup (facts_of facts) name of
     NONE => NONE
@@ -191,18 +198,31 @@
   end;
 
 
-(* static content *)
+(* content *)
+
+local
+
+fun included verbose prev_facts facts name =
+  not (exists (fn prev => defined prev name) prev_facts orelse
+    not verbose andalso is_concealed facts name);
+
+in
 
 fun fold_static f =
-  Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
+  Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
 
 fun dest_static verbose prev_facts facts =
-  fold_static (fn (name, ths) =>
-    if exists (fn prev => defined prev name) prev_facts orelse
-      not verbose andalso is_concealed facts name then I
-    else cons (name, ths)) facts []
+  fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts []
   |> sort_by #1;
 
+fun dest_all context verbose prev_facts facts =
+  Name_Space.fold_table (fn (a, fact) =>
+    let val ths = (case fact of Static ths => ths | Dynamic f => f context)
+    in included verbose prev_facts facts a ? cons (a, ths) end) (facts_of facts) []
+  |> sort_by #1;
+
+end;
+
 
 (* indexed props *)