# HG changeset patch
# User wenzelm
# Date 1167491285 -3600
# Node ID 7120ef5bc37870e10387cc9dd6f20e46b106db46
# Parent  df2e82888a664cd4397ca0aed1c6e6ea48f41859
pretty_statement: more careful handling of name_hint;

diff -r df2e82888a66 -r 7120ef5bc378 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Dec 30 16:08:04 2006 +0100
+++ b/src/Pure/Isar/element.ML	Sat Dec 30 16:08:05 2006 +0100
@@ -226,9 +226,10 @@
 
 fun thm_name kind th prts =
   let val head =
-    (case PureThy.get_name_hint th of
-      "" => Pretty.command kind
-    | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
+    if PureThy.has_name_hint th then
+      Pretty.block [Pretty.command kind,
+        Pretty.brk 1, Pretty.str (Sign.base_name (PureThy.get_name_hint th) ^ ":")]
+    else Pretty.command kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
 fun obtain prop ctxt =