# HG changeset patch
# User paulson
# Date 1172663506 -3600
# Node ID 02fc0ceb094a6dc4ef473525704c920caa11bd8e
# Parent  c9f5895972b06d06e3e4102c99bf438bbba6bbc0
Now outputs metis calls

diff -r c9f5895972b0 -r 02fc0ceb094a src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Feb 28 11:12:12 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Feb 28 12:51:46 2007 +0100
@@ -357,7 +357,7 @@
               | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
         | doline hs (lname, t, deps) =
             hs ^ lname ^ ": \"" ^ string_of t ^ 
-            "\"\n  by (meson " ^ space_implode " " deps ^ ")\n"
+            "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
       fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
         | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
   in setmp show_sorts true dolines end;
@@ -513,8 +513,8 @@
 fun get_axiom_names_vamp proofstr thm_names =
    get_axiom_names thm_names (get_vamp_linenums proofstr);
     
-fun rules_to_string [] = "NONE"
-  | rules_to_string xs = space_implode "  " xs
+fun rules_to_metis [] = "metis"
+  | rules_to_metis xs = "metis (" ^ space_implode " " xs ^ ")"
 
 
 (*The signal handler in watcher.ML must be able to read the output of this.*)
@@ -522,7 +522,8 @@
  (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
          " num of clauses is " ^ string_of_int (Vector.length thm_names));
   signal_success probfile toParent ppid 
-    ("Lemmas used in automatic proof: " ^ rules_to_string (getax proofstr thm_names)))
+    ("Try this proof method: \n" ^ 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);
    TextIO.output (toParent, "Translation failed for the proof: " ^