tuned markup;
authorwenzelm
Fri Jan 14 16:00:11 2011 +0100 (2011-01-14)
changeset 41551791b139a6c1e
parent 41550 efa734d9b221
child 41552 c5e71fee3617
tuned markup;
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Fri Jan 14 15:44:47 2011 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Jan 14 16:00:11 2011 +0100
     1.3 @@ -80,12 +80,13 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun pretty_fact_name (kind, "") = Pretty.str kind
     1.8 -  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
     1.9 -      Pretty.str (Long_Name.base_name name), Pretty.str ":"];
    1.10 +fun pretty_fact_name (kind, "") = Pretty.command kind
    1.11 +  | pretty_fact_name (kind, name) =
    1.12 +      Pretty.block [Pretty.command kind, Pretty.brk 1,
    1.13 +        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
    1.14  
    1.15  fun pretty_facts ctxt =
    1.16 -  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    1.17 +  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
    1.18      map (single o ProofContext.pretty_fact_aux ctxt false);
    1.19  
    1.20  in