# HG changeset patch
# User wenzelm
# Date 1394487577 -3600
# Node ID 1403a22e5538248d2929f238c7ad3bf3318c0c42
# Parent  98d466e6de8ae916b2b522af7efc392a86ae0214
tuned message;

diff -r 98d466e6de8a -r 1403a22e5538 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 10 22:28:20 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 10 22:39:37 2014 +0100
@@ -1293,18 +1293,18 @@
         else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts));
 
     fun prt_sect _ _ _ [] = []
-      | prt_sect s sep prt xs =
-          [Pretty.block (Pretty.breaks (Pretty.str s ::
+      | prt_sect head sep prt xs =
+          [Pretty.block (Pretty.breaks (head ::
             flat (separate sep (map (single o prt) xs))))];
   in
     Pretty.block (Pretty.fbreaks
       (Pretty.str (name ^ ":") ::
-        prt_sect "fix" [] (Pretty.str o Binding.name_of o fst) fixes @
-        prt_sect "let" [Pretty.str "and"] prt_let
+        prt_sect (Pretty.keyword1 "fix") [] (Pretty.str o Binding.name_of o fst) fixes @
+        prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
           (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
         (if forall (null o #2) asms then []
-          else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @
-        prt_sect "subcases:" [] (Pretty.str o fst) cs))
+          else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
+        prt_sect (Pretty.str "subcases:") [] (Pretty.str o fst) cs))
   end;
 
 in