# HG changeset patch
# User paulson
# Date 1179924732 -7200
# Node ID e692e0a38bad68dd2b25652cd8b89b160fbe5d3b
# Parent  ffef77eed382a5eeef37b7b42274b68e6b2bb870
formatting

diff -r ffef77eed382 -r e692e0a38bad src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed May 23 07:00:18 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed May 23 14:52:12 2007 +0200
@@ -470,7 +470,7 @@
 val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c);
 
 fun signal_success probfile toParent ppid msg = 
-  (trace ("\nReporting Success for" ^ probfile ^ "\n" ^ msg);
+  (trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg);
    TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n");
    TextIO.output (toParent, probfile ^ "\n");
    TextIO.flushOut toParent;