fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 17:38:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 18:07:25 2010 +0200
@@ -41,7 +41,7 @@
      output: string,
      proof: string,
      internal_thm_names: string Vector.vector,
-     conjecture_shape: int list,
+     conjecture_shape: int list list,
      filtered_clauses: (string * thm) list}
   type prover =
     params -> minimize_command -> Time.time -> problem -> prover_result
@@ -112,7 +112,7 @@
    output: string,
    proof: string,
    internal_thm_names: string Vector.vector,
-   conjecture_shape: int list,
+   conjecture_shape: int list list,
    filtered_clauses: (string * thm) list}
 
 type prover =
@@ -681,15 +681,14 @@
        clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
        of this hack. *)
     let
-      val j0 = hd conjecture_shape
+      val j0 = hd (hd conjecture_shape)
       val seq = extract_clause_sequence output
       val name_map = extract_clause_formula_relation output
       fun renumber_conjecture j =
         AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
-        |> the_single
-        |> (fn s => find_index (curry (op =) s) seq + 1)
+        |> map (fn s => find_index (curry (op =) s) seq + 1)
     in
-      (conjecture_shape |> map renumber_conjecture,
+      (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
                              SOME s' => undo_ascii_of s'
@@ -800,6 +799,7 @@
                               explicit_apply probfile clauses
             val conjecture_shape =
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
+              |> map single
             val result =
               do_run false
               |> (fn (_, msecs0, _, SOME _) =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 17:38:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 18:07:25 2010 +0200
@@ -19,11 +19,11 @@
     bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val isar_proof_text:
-    string Symtab.table * bool * int * Proof.context * int list
+    string Symtab.table * bool * int * Proof.context * int list list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val proof_text:
-    bool -> string Symtab.table * bool * int * Proof.context * int list
+    bool -> string Symtab.table * bool * int * Proof.context * int list list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
 end;
@@ -66,7 +66,8 @@
   | mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
 
-val index_in_shape : int -> int list -> int = find_index o curry (op =)
+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 > 0 andalso num <= Vector.length thm_names andalso
   Vector.sub (thm_names, num - 1) <> ""
@@ -745,27 +746,33 @@
       nth hyp_ts (index_in_shape num conjecture_shape)
       handle Subscript =>
              raise Fail ("Cannot find hypothesis " ^ Int.toString num)
-    val concl_l = (raw_prefix, List.last conjecture_shape)
-    fun first_pass ([], contra) = ([], contra)
-      | first_pass ((step as Fix _) :: proof, contra) =
-        first_pass (proof, contra) |>> cons step
-      | first_pass ((step as Let _) :: proof, contra) =
-        first_pass (proof, contra) |>> cons step
-      | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
-        if l = concl_l then
-          first_pass (proof, contra ||> l = concl_l ? cons step)
-        else
-          first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
-      | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
-        let val step = Have (qs, l, t, ByMetis (ls, ss)) in
-          if exists (member (op =) (fst contra)) ls then
-            first_pass (proof, contra |>> cons l ||> cons step)
-          else
-            first_pass (proof, contra) |>> cons step
-        end
-      | first_pass _ = raise Fail "malformed proof"
+     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
+     val canonicalize_labels =
+       map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
+       #> distinct (op =)
+     fun first_pass ([], contra) = ([], contra)
+       | first_pass ((step as Fix _) :: proof, contra) =
+         first_pass (proof, contra) |>> cons step
+       | first_pass ((step as Let _) :: proof, contra) =
+         first_pass (proof, contra) |>> cons step
+       | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
+         if member (op =) concl_ls l then
+           first_pass (proof, contra ||> l = hd concl_ls ? cons step)
+         else
+           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
+       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+         let
+           val ls = canonicalize_labels ls
+           val step = Have (qs, l, t, ByMetis (ls, ss))
+         in
+           if exists (member (op =) (fst contra)) ls then
+             first_pass (proof, contra |>> cons l ||> cons step)
+           else
+             first_pass (proof, contra) |>> cons step
+         end
+       | first_pass _ = raise Fail "malformed proof"
     val (proof_top, (contra_ls, contra_proof)) =
-      first_pass (proof, ([concl_l], []))
+      first_pass (proof, (concl_ls, []))
     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
     fun backpatch_labels patches ls =
       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
@@ -800,7 +807,7 @@
                val proofs =
                  map_filter
                      (fn l =>
-                         if l = concl_l then
+                         if member (op =) concl_ls l then
                            NONE
                          else
                            let