# HG changeset patch
# User wenzelm
# Date 1524664995 -7200
# Node ID 7eb532e4f8c0c245f9f2c8bf646d60d759e91bda
# Parent  6d7cc6723978c2e4e51bcb2a583cc2a117c45f78# Parent  4c9e79aeadf0b5b5d5e5051099f293319e7bbc14
merged

diff -r 6d7cc6723978 -r 7eb532e4f8c0 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Apr 25 13:29:21 2018 +0000
+++ b/src/Pure/more_thm.ML	Wed Apr 25 16:03:15 2018 +0200
@@ -603,10 +603,9 @@
 
 (* unofficial theorem names *)
 
+fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN;
 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
-
-val has_name_hint = can the_name_hint;
-val get_name_hint = the_default "??.unknown" o try the_name_hint;
+fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown";
 
 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);