# HG changeset patch
# User blanchet
# Date 1392190648 -3600
# Node ID 4d2123c583fa7bcbf9c7fdadd7fc444419ef7aa4
# Parent  8b7c7157fa11232be7bdb91ef0f1e161ea7c3463
tuned message

diff -r 8b7c7157fa11 -r 4d2123c583fa src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- 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)