# HG changeset patch
# User wenzelm
# Date 1392921514 -3600
# Node ID 8103021024c1ca5dc77991c64a883da3fe4c6f64
# Parent  95c8ef02f04b4827229653c6a7ce0f328abd40d4
prefer cat_lines;

diff -r 95c8ef02f04b -r 8103021024c1 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 20 19:32:20 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 20 19:38:34 2014 +0100
@@ -531,7 +531,7 @@
        |> AList.group (op =)
        |> map (fn (a, xs) => string_for_annotation a ^ ": " ^
                              string_for_vars ", " (sort int_ord xs))
-       |> space_implode "\n"))
+       |> cat_lines))
 
 (* The ML solver timeout should correspond more or less to the overhead of invoking an external
    prover. *)
diff -r 95c8ef02f04b -r 8103021024c1 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 20 19:32:20 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 20 19:38:34 2014 +0100
@@ -209,7 +209,7 @@
          (if null iters then [] else ["iter: " ^ commas (map implode iters)]) @
          miscs of
       [] => "empty"
-    | lines => space_implode "\n" lines
+    | lines => cat_lines lines
   end
 
 fun scopes_equivalent (s1 : scope, s2 : scope) =
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))
diff -r 95c8ef02f04b -r 8103021024c1 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Thu Feb 20 19:32:20 2014 +0100
+++ b/src/Tools/coherent.ML	Thu Feb 20 19:38:34 2014 +0100
@@ -119,7 +119,7 @@
 val show_facts = Unsynchronized.ref false;
 
 fun string_of_facts ctxt s facts =
-  space_implode "\n"
+  cat_lines
     (s :: map (Syntax.string_of_term ctxt)
       (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
 
@@ -175,8 +175,8 @@
 fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   let
     val _ =
-      message (fn () => space_implode "\n"
-        ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
+      message (fn () =>
+        cat_lines ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
     val th' =
       Drule.implies_elim_list
         (Thm.instantiate