tuned message;
authorwenzelm
Sat Apr 26 22:43:22 2014 +0200 (2014-04-26)
changeset 56760ef5df088e022
parent 56759 790f7562cd0e
child 56761 951c6a9ac3d7
tuned message;
src/Pure/Tools/find_consts.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sat Apr 26 22:35:19 2014 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Apr 26 22:43:22 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_const ctxt) matches
     1.8 +    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);