# HG changeset patch
# User wenzelm
# Date 1295017211 -3600
# Node ID 791b139a6c1e24f7c7886758e44088c77bb519de
# Parent  efa734d9b22128b5613dda731bc410a7630a52a6
tuned markup;

diff -r efa734d9b221 -r 791b139a6c1e src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 14 15:44:47 2011 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 14 16:00:11 2011 +0100
@@ -80,12 +80,13 @@
 
 local
 
-fun pretty_fact_name (kind, "") = Pretty.str kind
-  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
-      Pretty.str (Long_Name.base_name name), Pretty.str ":"];
+fun pretty_fact_name (kind, "") = Pretty.command kind
+  | pretty_fact_name (kind, name) =
+      Pretty.block [Pretty.command kind, Pretty.brk 1,
+        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
-  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
+  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
     map (single o ProofContext.pretty_fact_aux ctxt false);
 
 in