diff -r 95c8ef02f04b -r 8103021024c1 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 20 19:32:20 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 20 19:38:34 2014 +0100
@@ -25,7 +25,7 @@
 fun print_intross options thy msg intross =
   if show_intermediate_results options then
     tracing (msg ^
-      (space_implode "\n" (map
+      (cat_lines (map
         (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
            commas (map (Display.string_of_thm_global thy) intros)) intross)))
   else ()
@@ -34,8 +34,8 @@
   if show_intermediate_results options then
     map (fn (c, thms) =>
       "Constant " ^ c ^ " has specification:\n" ^
-        (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
-    |> space_implode "\n" |> tracing
+        (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+    |> cat_lines |> tracing
   else ()
 
 fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))