diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -170,7 +170,7 @@
       val eqth = introduce_combinators_in_cterm ctxt (Thm.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 ^
+           (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^
               "\nException message: " ^ msg);
             (* A type variable of sort "{}" will make "abstraction" fail. *)
             TrueI)