# HG changeset patch
# User wenzelm
# Date 1524658424 -7200
# Node ID 4c9e79aeadf0b5b5d5e5051099f293319e7bbc14
# Parent  412fe0623c5d1619ef44ccbb17d293ea2a8ba58f
tuned -- avoid spurious exception trace for "the";

diff -r 412fe0623c5d -r 4c9e79aeadf0 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Apr 24 22:22:25 2018 +0100
+++ b/src/Pure/more_thm.ML	Wed Apr 25 14:13:44 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);