# HG changeset patch
# User wenzelm
# Date 1690293152 -7200
# Node ID 3023063833e4e0dcaaabc287e8e34acf62bdaae7
# Parent  127e4e952446e10db2536594c0129eea5809435d
tuned;

diff -r 127e4e952446 -r 3023063833e4 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Tue Jul 25 15:04:17 2023 +0200
+++ b/src/Pure/Thy/bibtex.ML	Tue Jul 25 15:52:32 2023 +0200
@@ -49,7 +49,7 @@
     fun decode yxml =
       let
         val props = XML.Decode.properties (YXML.parse_body yxml);
-        val name = the_default "" (Properties.get props Markup.nameN);
+        val name = Properties.get_string props Markup.nameN;
         val pos = Position.of_properties props;
       in (name, pos) end;
   in
diff -r 127e4e952446 -r 3023063833e4 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 25 15:04:17 2023 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 25 15:52:32 2023 +0200
@@ -615,7 +615,7 @@
 
 val theoremK = "theorem";
 
-fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
+fun legacy_get_kind thm = Properties.get_string (Thm.get_tags thm) Markup.kindN;
 
 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;