# HG changeset patch
# User wenzelm
# Date 1452953035 -3600
# Node ID 74c56f8b68e812acc5a9b27922a1b57d54e7f7b1
# Parent  d54e916b8b65002396fef1ead632fd6786158228
tuned message;

diff -r d54e916b8b65 -r 74c56f8b68e8 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Jan 16 15:03:40 2016 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sat Jan 16 15:03:55 2016 +0100
@@ -305,12 +305,16 @@
     Pretty.quote (Syntax.pretty_typ ctxt T)];
 
 fun pretty_vars pos ctxt kind vs =
-  Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs));
+  Pretty.block
+    (Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs));
+
+val fixes = (Markup.keyword2, "fixes");
+val consts = (Markup.keyword1, "consts");
 
 fun pretty_consts pos ctxt pred cs =
   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
-    [] => pretty_vars pos ctxt "constants" cs
-  | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]);
+    [] => pretty_vars pos ctxt consts cs
+  | ps => Pretty.chunks [pretty_vars pos ctxt fixes ps, pretty_vars pos ctxt consts cs]);
 
 in