--- 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)