src/Pure/Isar/proof_context.ML

   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
   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
   val read_class: Proof.context -> string -> class
   val read_typ: Proof.context -> string -> typ

     if Facts.defined local_facts name
     then local_facts else global_facts
   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;
 
 
 
 (** pretty printing **)
 
 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
     val pretty_thm = Thm.pretty_thm ctxt;
     val pretty_thms = map (Thm.pretty_thm_item ctxt);