# HG changeset patch
# User wenzelm
# Date 1430667406 -7200
# Node ID 5901cb4db0ae1f8501c9e3f4af9cb031a5ccf1a8
# Parent  3a8501876dbaca070f278c482f1f4466a9312e34
tuned output;

diff -r 3a8501876dba -r 5901cb4db0ae src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun May 03 17:19:27 2015 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun May 03 17:36:46 2015 +0200
@@ -160,11 +160,13 @@
   | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
 
 fun pretty_binding ctxt (b, atts) sep =
-  if is_empty_binding (b, atts) then []
-  else if Binding.is_empty b then
-    [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
-  else
-    [Pretty.block (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])];
+  (case (Binding.is_empty b, null atts) of
+    (true, true) => []
+  | (false, true) => [Pretty.block [Binding.pretty b, Pretty.str sep]]
+  | (true, false) => [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])]
+  | (false, false) =>
+      [Pretty.block
+        (Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])]);
 
 
 (* get attributes *)