src/HOL/Tools/Meson/meson_clausify.ML

     let
       val th = Drule.eta_contraction_rule th
       val eqth = introduce_combinators_in_cterm (cprop_of th)
     in Thm.equal_elim eqth th end
     handle THM (msg, _, _) =>
-           (warning ("Error in the combinator translation of " ^
-                     Display.string_of_thm ctxt th ^
-                     "\nException message: " ^ msg ^ ".");
+           (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^
+              "\nException message: " ^ msg);
             (* A type variable of sort "{}" will make "abstraction" fail. *)
             TrueI)
 
 (*cterms are used throughout for efficiency*)
 val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;