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