tuned markup;
authorwenzelm
Thu, 09 Sep 2010 21:44:52 +0200
changeset 39284 3aefd3342978
parent 39283 635e09dea465
child 39285 85728a4b5620
tuned markup;
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,