--- a/src/HOL/Tools/Meson/meson_clausify.ML Sun Feb 16 21:09:47 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Feb 16 21:33:28 2014 +0100
@@ -172,9 +172,8 @@
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)