--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Feb 12 08:37:28 2014 +0100
@@ -307,7 +307,7 @@
val (_, ts) = strip_comb t
in
print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^
- "splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
+ " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
THEN TRY (Splitter.split_asm_tac [split_asm] 1
THEN (print_tac options "after splitting with split_asm rules")
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)