diff -r 0f3c375fd27c -r 734f7e6151c9 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Thu May 08 11:47:38 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML	Thu May 08 13:47:17 2014 +0200
@@ -114,15 +114,12 @@
       |> map (apsnd fst o snd);
   in
     Pretty.block
-      (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
-        Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
+      (Pretty.fbreaks (Pretty.keyword1 "find_consts" :: map pretty_criterion raw_criteria)) ::
     Pretty.str "" ::
-    Pretty.str
-     (if null matches
-      then "nothing found"
-      else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
-    Pretty.str "" ::
-    grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches
+    (if null matches then [Pretty.str "found nothing"]
+     else
+       Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") ::
+       grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches)
   end |> Pretty.fbreaks |> curry Pretty.blk 0;
 
 fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);