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