--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sun Dec 20 12:50:48 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Dec 20 13:03:41 2015 +0100
@@ -368,16 +368,13 @@
in
if null non_trivial_assms then ()
else
- let
- val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
- Pretty.str thm_name,
- Pretty.str " transfer rule found:",
- Pretty.brk 1] @
- ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
- [Pretty.str "."])
- in
- warning (Pretty.str_of pretty_msg)
- end
+ Pretty.block ([Pretty.str "Non-trivial assumptions in ",
+ Pretty.str thm_name,
+ Pretty.str " transfer rule found:",
+ Pretty.brk 1] @
+ Pretty.commas (map (Syntax.pretty_term ctxt) non_trivial_assms))
+ |> Pretty.string_of
+ |> warning
end
end