# HG changeset patch
# User paulson
# Date 1524670829 -3600
# Node ID 362baebe25a57e5dbfc623ee34f1ed3092949fd4
# Parent  7eb532e4f8c0c245f9f2c8bf646d60d759e91bda# Parent  67b39890158c617e3187afa7125e1bed87f6f6c8
merged

diff -r 67b39890158c -r 362baebe25a5 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Apr 25 15:36:48 2018 +0100
+++ b/src/Pure/more_thm.ML	Wed Apr 25 16:40:29 2018 +0100
@@ -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);