src/Pure/Isar/proof_display.ML
changeset 39284 3aefd3342978
parent 36610 bafd82950e24
child 39557 fe5722fce758
     1.1 --- a/src/Pure/Isar/proof_display.ML	Fri Sep 10 15:55:09 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Sep 09 21:44:52 2010 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4  fun print_results do_print ctxt ((kind, name), facts) =
     1.5    if not do_print orelse kind = "" then ()
     1.6    else if name = "" then
     1.7 -    Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
     1.8 +    Pretty.writeln (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
     1.9    else Pretty.writeln
    1.10      (case facts of
    1.11        [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,