# HG changeset patch
# User wenzelm
# Date 1450613021 -3600
# Node ID 669f473972499b9541c701609459d251a8970407
# Parent  5348b76aa94cc75750531837757b08f7216cef06
proper formatting via Pretty.string_of;
tuned;

diff -r 5348b76aa94c -r 669f47397249 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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