tuned;
authorwenzelm
Sun, 27 Apr 2014 13:35:18 +0200
changeset 56763 70371621fdb6
parent 56762 539fe017905a
child 56764 5b6f4655e2f2
tuned;
src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat Apr 26 22:57:51 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML	Sun Apr 27 13:35:18 2014 +0200
@@ -120,7 +120,7 @@
       then "nothing found"
       else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
     Pretty.str "" ::
-    map (Pretty.item o single o pretty_const ctxt) matches
+    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);