# HG changeset patch
# User blanchet
# Date 1280156950 -7200
# Node ID 11c076ea92e9f09e5df3b1c6476a8e91fa22e2f7
# Parent  06f02b15ef8a04de8f14448ee5acd961b20ed72a
simplify "conjecture_shape" business, as a result of using FOF instead of CNF

diff -r 06f02b15ef8a -r 11c076ea92e9 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jul 26 17:03:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jul 26 17:09:10 2010 +0200
@@ -43,7 +43,7 @@
      output: string,
      proof: string,
      internal_thm_names: string Vector.vector,
-     conjecture_shape: int list list,
+     conjecture_shape: int list,
      filtered_clauses: ((string * int) * 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 list,
+   conjecture_shape: int list,
    filtered_clauses: ((string * int) * thm) list}
 
 type prover =
diff -r 06f02b15ef8a -r 11c076ea92e9 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:03:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:09:10 2010 +0200
@@ -287,8 +287,7 @@
                                               thm_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
     let
-      (* FIXME: hd of head once clausification is left to the ATP *)
-      val j0 = hd (List.concat conjecture_shape)
+      val j0 = hd conjecture_shape
       val seq = extract_clause_sequence output
       val name_map = extract_clause_formula_relation output
       fun renumber_conjecture j =
@@ -296,7 +295,7 @@
         |> the_single
         |> (fn s => find_index (curry (op =) s) seq + 1)
     in
-      (conjecture_shape |> map (map renumber_conjecture),
+      (conjecture_shape |> map 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'
@@ -404,7 +403,6 @@
                             explicit_apply probfile clauses
           val conjecture_shape =
             conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
-            |> map single (* ### FIXME: get rid of "map single" *)
           val result =
             do_run false
             |> (fn (_, msecs0, _, SOME _) =>
diff -r 06f02b15ef8a -r 11c076ea92e9 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 17:03:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 17:09:10 2010 +0200
@@ -14,11 +14,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 list
+    string Symtab.table * bool * int * Proof.context * int 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 list
+    bool -> string Symtab.table * bool * int * Proof.context * int list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
 end;
@@ -36,8 +36,7 @@
 fun mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
 
-val index_in_shape : int -> int list list -> int =
-  find_index o exists o curry (op =)
+val index_in_shape : int -> int list -> int = find_index 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) <> ""
@@ -708,25 +707,19 @@
        direct proof, introducing case splits when an inference depends on
        several facts that depend on the negated conjecture. *)
     fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
-    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 =)
+    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 member (op =) concl_ls l then
-          first_pass (proof, contra ||> l = hd concl_ls ? cons step)
+        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 ls = canonicalize_labels ls
-          val step = Have (qs, l, t, ByMetis (ls, ss))
-        in
+        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
@@ -734,7 +727,7 @@
         end
       | first_pass _ = raise Fail "malformed proof"
     val (proof_top, (contra_ls, contra_proof)) =
-      first_pass (proof, (concl_ls, []))
+      first_pass (proof, ([concl_l], []))
     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) ([], [])
@@ -769,7 +762,7 @@
                val proofs =
                  map_filter
                      (fn l =>
-                         if member (op =) concl_ls l then
+                         if l = concl_l then
                            NONE
                          else
                            let