--- 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);
--- a/src/Pure/Tools/find_theorems.ML Thu May 08 11:47:38 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML Thu May 08 13:47:17 2014 +0200
@@ -484,13 +484,12 @@
else ""));
in
Pretty.block
- (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
- Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
+ (Pretty.fbreaks (Pretty.keyword1 "find_theorems" :: map (pretty_criterion ctxt) criteria)) ::
Pretty.str "" ::
- (if null theorems then [Pretty.str "nothing found"]
+ (if null theorems then [Pretty.str "found nothing"]
else
- [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
- grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
+ Pretty.str (tally_msg ^ ":") ::
+ grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
end |> Pretty.fbreaks |> curry Pretty.blk 0;
end;