src/Pure/Isar/proof_display.ML
changeset 41551 791b139a6c1e
parent 39557 fe5722fce758
child 42360 da8817d01e7c
     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