# HG changeset patch
# User wenzelm
# Date 1284061492 -7200
# Node ID 3aefd3342978de4f57701a293d148d2532b537e1
# Parent  635e09dea4655470720e8714a5e54b984ca4d888
tuned markup;

diff -r 635e09dea465 -r 3aefd3342978 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Sep 10 15:55:09 2010 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Sep 09 21:44:52 2010 +0200
@@ -93,7 +93,7 @@
 fun print_results do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
-    Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+    Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else Pretty.writeln
     (case facts of
       [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,