diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -306,7 +306,7 @@
             val (_, ts) = strip_comb t
           in
             trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
-              " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
+              " splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm)
             THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
               THEN (trace_tac ctxt options "after splitting with split_asm rules")
             (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)