proper formatting via Pretty.string_of;
authorwenzelm
Sun, 20 Dec 2015 13:03:41 +0100
changeset 61878 669f47397249
parent 61877 5348b76aa94c
child 61879 276ad4354069
proper formatting via Pretty.string_of; tuned;
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