Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 25 Jul 2023 15:52:32 +0200
changeset 78462 3023063833e4
parent 78455 127e4e952446
child 78463 c956b43749f0
tuned;
src/Pure/Thy/bibtex.ML file | annotate | diff | comparison | revisions
src/Pure/more_thm.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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;
isabelle