keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
this is rather involved because the Flotter FOF-to-CNF translator is normally implicit.
We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Fri Jul 23 21:29:29 2010 +0200
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+#
+# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
+# Isar proof reconstruction)
+#
+# Author: Jasmin Blanchette, TU Muenchen
+
+options=${@:1:$(($#-1))}
+name=${@:$(($#)):1}
+
+$SPASS_HOME/tptp2dfg $name $name.fof.dfg
+$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
+    | sed 's/description({$/description({*/' \
+    > $name.cnf.dfg
+rm -f $name.fof.dfg
+cat $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg
+rm -f $name.cnf.dfg

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jul 23 15:04:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jul 23 21:29:29 2010 +0200
@@ -239,6 +239,43 @@
        class_rel_clauses, arity_clauses))
   end
 
+fun extract_clause_sequence output =
+  let
+    val tokens_of = String.tokens (not o Char.isAlphaNum)
+    fun extract_num ("clause" :: (ss as _ :: _)) =
+    Int.fromString (List.last ss)
+      | extract_num _ = NONE
+  in output |> split_lines |> map_filter (extract_num o tokens_of) end
+
+val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
+
+val parse_clause_formula_pair =
+  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+  --| Scan.option ($$ ",")
+val parse_clause_formula_relation =
+  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
+  |-- Scan.repeat parse_clause_formula_pair
+val extract_clause_formula_relation =
+  Substring.full
+  #> Substring.position set_ClauseFormulaRelationN
+  #> snd #> Substring.string #> strip_spaces #> explode
+  #> parse_clause_formula_relation #> fst
+
+fun repair_theorem_names output thm_names =
+  if String.isSubstring set_ClauseFormulaRelationN output then
+    let
+      val seq = extract_clause_sequence output
+      val name_map = extract_clause_formula_relation output
+    in
+      seq |> map (the o AList.lookup (op =) name_map)
+          |> map (fn s => case try (unprefix axiom_prefix) s of
+                            SOME s' => undo_ascii_of s'
+                          | NONE => "")
+          |> Vector.fromList
+    end
+  else
+    thm_names
+
 
 (* generic TPTP-based provers *)
 
@@ -298,15 +335,7 @@
         (if Config.get ctxt measure_runtime then
            "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
          else
-           "exec " ^ core) ^ " 2>&1" ^
-        (if overlord then
-           " | sed 's/,/, /g' \
-           \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \
-           \| sed 's/  / /g' | sed 's/| |/||/g' \
-           \| sed 's/ = = =/===/g' \
-           \| sed 's/= = /== /g'"
-         else
-           "")
+           "exec " ^ core) ^ " 2>&1"
       end
     fun split_time s =
       let
@@ -320,7 +349,9 @@
         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
       in (output, as_time t) end;
     fun run_on probfile =
-      if File.exists command then
+      if home = "" then
+        error ("The environment variable " ^ quote home_var ^ " is not set.")
+      else if File.exists command then
         let
           fun do_run complete =
             let
@@ -350,8 +381,6 @@
                           (output, msecs0 + msecs, proof, outcome))
                  | result => result)
         in ((pool, conjecture_shape), result) end
-      else if home = "" then
-        error ("The environment variable " ^ quote home_var ^ " is not set.")
       else
         error ("Bad executable: " ^ Path.implode command ^ ".");
 
@@ -367,6 +396,7 @@
 
     val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
       with_path cleanup export run_on (prob_pathname subgoal)
+    val internal_thm_names = repair_theorem_names output internal_thm_names
 
     val (message, relevant_thm_names) =
       case outcome of
@@ -417,11 +447,11 @@
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of "hAPP". *)
 val spass_config : prover_config =
-  {home_var = "SPASS_HOME",
-   executable = "SPASS",
+  {home_var = "ISABELLE_ATP_MANAGER",
+   executable = "SPASS_TPTP",
    (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
-     ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
+     ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^
       string_of_int (to_generous_secs timeout div 2))
      |> not complete ? prefix "-SOS=1 ",
@@ -432,8 +462,7 @@
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
-      (OldSpass, "unrecognized option `-TPTP'"),
-      (OldSpass, "Unrecognized option TPTP")],
+      (OldSpass, "tptp2dfg")],
    max_axiom_clauses = 40,
    prefers_theory_relevant = true}
 val spass = tptp_prover "spass" spass_config

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jul 23 15:04:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jul 23 21:29:29 2010 +0200
@@ -33,12 +33,11 @@
 
 type minimize_command = string list -> string
 
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-
 val index_in_shape : int -> int list list -> int =
   find_index o exists o curry (op =)
-fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
+fun is_axiom_clause_number thm_names num =
+  num > 0 andalso num <= Vector.length thm_names andalso
+  Vector.sub (thm_names, num - 1) <> ""
 fun is_conjecture_clause_number conjecture_shape num =
   index_in_shape num conjecture_shape >= 0
 
@@ -57,23 +56,6 @@
 
 (**** PARSING OF TSTP FORMAT ****)
 
-fun strip_spaces_in_list [] = ""
-  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
-  | strip_spaces_in_list [c1, c2] =
-    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
-  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
-    if Char.isSpace c1 then
-      strip_spaces_in_list (c2 :: c3 :: cs)
-    else if Char.isSpace c2 then
-      if Char.isSpace c3 then
-        strip_spaces_in_list (c1 :: c3 :: cs)
-      else
-        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
-        strip_spaces_in_list (c3 :: cs)
-    else
-      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
-
 (* Syntax trees, either term list or formulae *)
 datatype node = IntLeaf of int | StrNode of string * node list
 
@@ -85,9 +67,6 @@
 (*Strings enclosed in single quotes, e.g. filenames*)
 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
 
-(*Integer constants, typically proof line numbers*)
-val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
 val parse_dollar_name =
   Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
 
@@ -102,7 +81,7 @@
    forever at compile time. *)
 fun parse_term pool x =
      (parse_quoted >> str_leaf
-   || parse_integer >> IntLeaf
+   || scan_integer >> IntLeaf
    || (parse_dollar_name >> repair_name pool)
       -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
    || $$ "(" |-- parse_term pool --| $$ ")"
@@ -149,11 +128,11 @@
 fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
 fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
 fun parse_tstp_line pool =
-     ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
+     ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ ","
        --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
        --| parse_tstp_annotations --| $$ ")" --| $$ "."
       >> finish_tstp_definition_line)
-  || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
+  || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ ","
        --| Symbol.scan_id --| $$ "," -- parse_clause pool
        -- parse_tstp_annotations --| $$ ")" --| $$ "."
       >> finish_tstp_inference_line)
@@ -162,7 +141,7 @@
 
 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
    is not clear anyway. *)
-val parse_dot_name = parse_integer --| $$ "." --| parse_integer
+val parse_dot_name = scan_integer --| $$ "." --| scan_integer
 
 val parse_spass_annotations =
   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
@@ -185,7 +164,7 @@
    <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
 fun parse_spass_line pool =
-  parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+  scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   >> finish_spass_line
 
@@ -535,7 +514,7 @@
    extracted. *)
 fun extract_formula_numbers_in_atp_proof atp_proof =
   let
-    val tokens_of = String.tokens (not o is_ident_char)
+    val tokens_of = String.tokens (not o Char.isAlphaNum)
     fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
       | extract_num _ = NONE

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jul 23 15:04:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jul 23 21:29:29 2010 +0200
@@ -11,6 +11,7 @@
   type arity_clause = Metis_Clauses.arity_clause
   type fol_clause = Metis_Clauses.fol_clause
 
+  val axiom_prefix : string
   val write_tptp_file :
     theory -> bool -> bool -> bool -> Path.T
     -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
@@ -136,11 +137,11 @@
 
 (** Sledgehammer stuff **)
 
-val clause_prefix = "cls_"
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
 val arity_clause_prefix = "clsarity_"
 
-fun hol_ident axiom_name clause_id =
-  clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
+fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name
 
 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
 
@@ -189,8 +190,8 @@
   |> formula_for_fo_literals
 
 fun problem_line_for_axiom full_types
-        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
-  Fof (hol_ident axiom_name clause_id, kind,
+        (clause as FOLClause {axiom_name, kind, ...}) =
+  Fof (hol_ident axiom_prefix axiom_name, kind,
        formula_for_axiom full_types clause)
 
 fun problem_line_for_class_rel_clause
@@ -213,8 +214,8 @@
        |> formula_for_fo_literals)
 
 fun problem_line_for_conjecture full_types
-        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
-  Fof (hol_ident axiom_name clause_id, kind,
+        (clause as FOLClause {axiom_name, kind, literals, ...}) =
+  Fof (hol_ident conjecture_prefix axiom_name, kind,
        map (fo_literal_for_literal full_types) literals
        |> formula_for_fo_literals |> mk_anot)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 23 15:04:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 23 21:29:29 2010 +0200
@@ -9,8 +9,10 @@
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val timestamp : unit -> string
+  val strip_spaces : string -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
+  val scan_integer : string list -> int * string list
   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
@@ -31,6 +33,25 @@
 
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+
+fun strip_spaces_in_list [] = ""
+  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
+  | strip_spaces_in_list [c1, c2] =
+    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
+  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+    if Char.isSpace c1 then
+      strip_spaces_in_list (c2 :: c3 :: cs)
+    else if Char.isSpace c2 then
+      if Char.isSpace c3 then
+        strip_spaces_in_list (c1 :: c3 :: cs)
+      else
+        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
+        strip_spaces_in_list (c3 :: cs)
+    else
+      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
+val strip_spaces = strip_spaces_in_list o String.explode
+
 fun parse_bool_option option name s =
   (case s of
      "smart" => if option then NONE else raise Option
@@ -61,6 +82,9 @@
         SOME (Time.fromMilliseconds msecs)
     end
 
+fun is_head_digit s = Char.isDigit (String.sub (s, 0))
+val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+
 val subscript = implode o map (prefix "\<^isub>") o explode
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript