# HG changeset patch
# User paulson
# Date 1187713811 -7200
# Node ID cf2470f64b1de2cfbcb052201a40af033fcf76f2
# Parent  7cbaf94aed08c04385288f83e18386955a959e21
Modified message for sendback

diff -r 7cbaf94aed08 -r cf2470f64b1d src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Aug 21 18:27:41 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Aug 21 18:30:11 2007 +0200
@@ -541,7 +541,7 @@
  (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
          " num of clauses is " ^ string_of_int (Vector.length thm_names));
   signal_success probfile toParent ppid
-    ("Try this command: \n  apply " ^ rules_to_metis (getax proofstr thm_names))
+    ("apply " ^ rules_to_metis (getax proofstr thm_names))
  )
  handle e => (*FIXME: exn handler is too general!*)
   (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);