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;