# HG changeset patch
# User wenzelm
# Date 1718022573 -7200
# Node ID d90a96894644c78a4612f49e89073a630ffc73ce
# Parent  559909bd7715a5273ad8b97cf4de9dc24302ed68
more robust / permissive;

diff -r 559909bd7715 -r d90a96894644 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jun 10 14:05:39 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 10 14:29:33 2024 +0200
@@ -414,14 +414,15 @@
     then local_facts else global_facts
   end;
 
-fun markup_extern_fact ctxt 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;
+fun markup_extern_fact _ "" = ([], "")
+  | markup_extern_fact ctxt 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;
 
 fun pretty_thm_name ctxt (name, i) =
   Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i);