src/Pure/Tools/find_consts.ML
changeset 56763 70371621fdb6
parent 56760 ef5df088e022
child 56891 48899c43b07d
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sat Apr 26 22:57:51 2014 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Apr 27 13:35:18 2014 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4        then "nothing found"
     1.5        else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
     1.6      Pretty.str "" ::
     1.7 -    map (Pretty.item o single o pretty_const ctxt) matches
     1.8 +    grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches
     1.9    end |> Pretty.fbreaks |> curry Pretty.blk 0;
    1.10  
    1.11  fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);