renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
"full" sounds like "full types" or something, not like a structured Isar proof -- at some point I hope to make this an option that's orthogonal to the prover

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 15:33:18 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 16:04:15 2010 +0100
@@ -184,7 +184,7 @@
   emit_structured_proof = full};
 
 val vampire = tptp_prover ("vampire", vampire_prover_config false);
-val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
+val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
 
 
 (* E prover *)
@@ -206,7 +206,7 @@
   emit_structured_proof = full};
 
 val eprover = tptp_prover ("e", eprover_config false);
-val eprover_full = tptp_prover ("e_full", eprover_config true);
+val eprover_isar = tptp_prover ("e_isar", eprover_config true);
 
 
 (* SPASS *)
@@ -290,7 +290,7 @@
   "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
 
 val provers =
-  [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc,
+  [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
    remote_vampire, remote_spass, remote_eprover]
 val prover_setup = fold add_prover provers
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Mar 19 15:33:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Mar 19 16:04:15 2010 +0100
@@ -428,26 +428,33 @@
 fun isar_header [] = proofstart
   | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
 
-fun decode_tstp_file cnfs ctxt th sgno thm_names =
-  let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n")
-      val tuples = map (dest_tstp o tstp_line o explode) cnfs
-      val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n")
-      val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
-      val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
-      val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n")
-      val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
-      val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
-      val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
-      val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n")
-      val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
-      val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n")
-      val ccls = map forall_intr_vars ccls
-      val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
-      val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
-      val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n")
-  in
-    isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
-  end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
+fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
+  let
+    val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
+    val tuples = map (dest_tstp o tstp_line o explode) cnfs
+    val _ = trace_proof_msg (fn () =>
+      Int.toString (length tuples) ^ " tuples extracted\n")
+    val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
+    val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
+    val _ = trace_proof_msg (fn () =>
+      Int.toString (length raw_lines) ^ " raw_lines extracted\n")
+    val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
+    val _ = trace_proof_msg (fn () =>
+      Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
+    val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
+    val _ = trace_proof_msg (fn () =>
+      Int.toString (length lines) ^ " lines extracted\n")
+    val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
+    val _ = trace_proof_msg (fn () =>
+      Int.toString (length ccls) ^ " conjecture clauses\n")
+    val ccls = map forall_intr_vars ccls
+    val _ = app (fn th => trace_proof_msg
+                              (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
+    val isar_lines = isar_lines ctxt (map prop_of ccls)
+                                (stringify_deps thm_names [] lines)
+    val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
+  in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end
+  handle STREE _ => error "Could not extract proof (ATP output malformed?)";
 
 
 (*=== EXTRACTING PROOF-TEXT === *)
@@ -530,19 +537,17 @@
 (* atp_minimize [atp=<prover>] <lemmas> *)
 fun minimize_line _ [] = ""
   | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
-        (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
-                                         space_implode " " (kill_chained lemmas))
-
-val sendback_metis_no_chained =
-  Markup.markup Markup.sendback o metis_line o kill_chained
+        Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
+                                       space_implode " " (kill_chained lemmas))
 
 fun metis_lemma_list dfg name result =
-  let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
-  in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^
-    (if used_conj then
-       ""
-     else
-       "\nWarning: The goal is provable because the context is inconsistent."),
+  let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
+    (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
+     minimize_line name lemmas ^
+     (if used_conj then
+        ""
+      else
+        "\nWarning: The goal is provable because the context is inconsistent."),
      kill_chained lemmas)
   end;
 
@@ -551,15 +556,17 @@
   let
     (* Could use "split_lines", but it can return blank lines *)
     val lines = String.tokens (equal #"\n");
-    val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c)
+    val kill_spaces =
+      String.translate (fn c => if Char.isSpace c then "" else str c)
     val extract = get_proof_extract proof
     val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
     val (one_line_proof, lemma_names) = metis_lemma_list false name result
-    val structured =
-      if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
-      else decode_tstp_file cnfs ctxt goal subgoalno thm_names
+    val tokens = String.tokens (fn c => c = #" ") one_line_proof
+    val isar_proof =
+      if member (op =) tokens chained_hint then ""
+      else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
   in
-    (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured,
+    (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
      lemma_names)
   end