don't choke on synonyms when parsing SPASS's Flotter output + renamings;
the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 29 23:37:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Jul 30 00:02:25 2010 +0200
@@ -16,9 +16,9 @@
     TConsLit of name * name * name list |
     TVarLit of name * name
   datatype arity_clause =
-    ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   datatype class_rel_clause =
-    ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
+    ClassRelClause of {name: string, subclass: name, superclass: name}
   datatype combtyp =
     CombTVar of name |
     CombTFree of name |
@@ -84,8 +84,6 @@
 val tvar_prefix = "T_";
 val tfree_prefix = "t_";
 
-val class_rel_clause_prefix = "clsrel_";
-
 val const_prefix = "c_";
 val type_const_prefix = "tc_";
 val class_prefix = "class_";
@@ -259,7 +257,7 @@
   TVarLit of name * name
 
 datatype arity_clause =
-  ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
 
 
 fun gen_TVars 0 = []
@@ -271,12 +269,12 @@
     (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
 
 (*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
+fun make_axiom_arity_clause (tcons, name, (cls,args)) =
   let
     val tvars = gen_TVars (length args)
     val tvars_srts = ListPair.zip (tvars, args)
   in
-    ArityClause {axiom_name = axiom_name, 
+    ArityClause {name = name, 
                  conclLit = TConsLit (`make_type_class cls,
                                       `make_fixed_type_const tcons,
                                       tvars ~~ tvars),
@@ -287,7 +285,7 @@
 (**** Isabelle class relations ****)
 
 datatype class_rel_clause =
-  ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
+  ClassRelClause of {name: string, subclass: name, superclass: name}
 
 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
 fun class_pairs _ [] _ = []
@@ -299,10 +297,9 @@
       in fold add_supers subs [] end
 
 fun make_class_rel_clause (sub,super) =
-  ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^
-                               ascii_of super,
+  ClassRelClause {name = sub ^ "_" ^ super,
                   subclass = `make_type_class sub,
-                  superclass = `make_type_class super};
+                  superclass = `make_type_class super}
 
 fun make_class_rel_clauses thy subs supers =
   map make_class_rel_clause (class_pairs thy subs supers);

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 23:37:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jul 30 00:02:25 2010 +0200
@@ -162,7 +162,7 @@
 (* Clause preparation *)
 
 datatype fol_formula =
-  FOLFormula of {formula_name: string,
+  FOLFormula of {name: string,
                  kind: kind,
                  combformula: (name, combterm) formula,
                  ctypes_sorts: typ list}
@@ -296,7 +296,7 @@
   in t |> exists_subterm is_Var t ? aux end
 
 (* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp (formula_name, kind, t) =
+fun make_formula ctxt presimp (name, kind, t) =
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> transform_elim_term
@@ -309,8 +309,8 @@
               |> kind = Conjecture ? freeze_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
-    FOLFormula {formula_name = formula_name, combformula = combformula,
-                kind = kind, ctypes_sorts = ctypes_sorts}
+    FOLFormula {name = name, combformula = combformula, kind = kind,
+                ctypes_sorts = ctypes_sorts}
   end
 
 fun make_axiom ctxt presimp (name, th) =
@@ -433,15 +433,14 @@
                 (type_literals_for_types ctypes_sorts))
            (formula_for_combformula full_types combformula)
 
-fun problem_line_for_axiom full_types
-        (formula as FOLFormula {formula_name, kind, ...}) =
-  Fof (axiom_prefix ^ ascii_of formula_name, kind,
-       formula_for_axiom full_types formula)
+fun problem_line_for_fact prefix full_types
+                          (formula as FOLFormula {name, kind, ...}) =
+  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
 
-fun problem_line_for_class_rel_clause
-        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+                                                       superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
-    Fof (ascii_of axiom_name, Axiom,
+    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
                            AAtom (ATerm (superclass, [ty_arg]))]))
   end
@@ -451,17 +450,17 @@
   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
     (false, ATerm (c, [ATerm (sort, [])]))
 
-fun problem_line_for_arity_clause
-        (ArityClause {axiom_name, conclLit, premLits, ...}) =
-  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+                                                ...}) =
+  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
        mk_ahorn (map (formula_for_fo_literal o apfst not
                       o fo_literal_for_arity_literal) premLits)
                 (formula_for_fo_literal
                      (fo_literal_for_arity_literal conclLit)))
 
 fun problem_line_for_conjecture full_types
-        (FOLFormula {formula_name, kind, combformula, ...}) =
-  Fof (conjecture_prefix ^ formula_name, kind,
+                                (FOLFormula {name, kind, combformula, ...}) =
+  Fof (conjecture_prefix ^ name, kind,
        formula_for_combformula full_types combformula)
 
 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
@@ -608,14 +607,15 @@
                     file (conjectures, axioms, helper_facts, class_rel_clauses,
                           arity_clauses) =
   let
-    val axiom_lines = map (problem_line_for_axiom full_types) axioms
+    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+    val helper_lines =
+      map (problem_line_for_fact helper_prefix full_types) helper_facts
+    val conjecture_lines =
+      map (problem_line_for_conjecture full_types) conjectures
+    val tfree_lines = problem_lines_for_free_types conjectures
     val class_rel_lines =
       map problem_line_for_class_rel_clause class_rel_clauses
     val arity_lines = map problem_line_for_arity_clause arity_clauses
-    val helper_lines = map (problem_line_for_axiom full_types) helper_facts
-    val conjecture_lines =
-      map (problem_line_for_conjecture full_types) conjectures
-    val tfree_lines = problem_lines_for_free_types conjectures
     (* Reordering these might or might not confuse the proof reconstruction
        code or the SPASS Flotter hack. *)
     val problem =
@@ -647,7 +647,8 @@
 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
 
 val parse_clause_formula_pair =
-  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id
+  --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")"
   --| Scan.option ($$ ",")
 val parse_clause_formula_relation =
   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
@@ -673,8 +674,8 @@
         |> map (fn s => find_index (curry (op =) s) seq + 1)
     in
       (conjecture_shape |> map (maps renumber_conjecture),
-       seq |> map (the o AList.lookup (op =) name_map)
-           |> map (fn s => case try (unprefix axiom_prefix) s of
+       seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the
+                                  |> try (unprefix axiom_prefix) of
                              SOME s' => undo_ascii_of s'
                            | NONE => "")
            |> Vector.fromList)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 29 23:37:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jul 30 00:02:25 2010 +0200
@@ -12,6 +12,8 @@
 
   val axiom_prefix : string
   val conjecture_prefix : string
+  val helper_prefix : string
+  val class_rel_clause_prefix : string
   val arity_clause_prefix : string
   val tfrees_name : string
   val metis_line: bool -> int -> int -> string list -> string
@@ -40,7 +42,9 @@
 
 val axiom_prefix = "ax_"
 val conjecture_prefix = "conj_"
-val arity_clause_prefix = "clsarity_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "clrel_";
+val arity_clause_prefix = "arity_"
 val tfrees_name = "tfrees"
 
 (* Simple simplifications to ensure that sort annotations don't leave a trail of
@@ -500,7 +504,7 @@
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
     else if is_conjecture_number conjecture_shape num then
-      Inference (num, t, []) :: lines
+      Inference (num, negate_term t, []) :: lines
     else
       map (replace_deps_in_line (num, [])) lines
   | add_line _ _ (Inference (num, t, deps)) lines =