# HG changeset patch
# User blanchet
# Date 1275491188 -7200
# Node ID 0347b1a1668216e6ec3abd1b942e7967e5d7a1fb
# Parent  9d7cfae95b30877dea12eaf268540fe744e1b3d7
fix bug in direct Isar proofs, which was exhibited by the "BigO" example

diff -r 9d7cfae95b30 -r 0347b1a16682 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 15:18:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 17:06:28 2010 +0200
@@ -680,13 +680,12 @@
 val indent_size = 2
 val no_label = ("", ~1)
 
-fun no_show qs = not (member (op =) qs Show)
-
 (* When redirecting proofs, we keep information about the labels seen so far in
    the "backpatches" data structure. The first component indicates which facts
    should be associated with forthcoming proof steps. The second component is a
-   pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
-   "drop_ls" are those that should be dropped in a case split. *)
+   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
+   become assumptions and "drop_ls" are the labels that should be dropped in a
+   case split. *)
 type backpatches = (label * facts) list * (label list * label list)
 
 fun used_labels_of_step (Have (_, _, _, by)) =
@@ -767,12 +766,16 @@
       | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
                             patches) =
         if member (op =) (snd (snd patches)) l andalso
+           not (member (op =) (fst (snd patches)) l) andalso
            not (AList.defined (op =) (fst patches) l) then
           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
         else
           (case List.partition (member (op =) contra_ls) ls of
              ([contra_l], co_ls) =>
-             if no_show qs then
+             if member (op =) qs Show then
+               second_pass end_qs (proof, assums,
+                                   patches |>> cons (contra_l, (co_ls, ss)))
+             else
                second_pass end_qs
                            (proof, assums,
                             patches |>> cons (contra_l, (l :: co_ls, ss)))
@@ -781,9 +784,6 @@
                          else
                            Have (qs, l, negate_term thy t,
                                  ByMetis (backpatch_label patches l)))
-             else
-               second_pass end_qs (proof, assums,
-                                   patches |>> cons (contra_l, (co_ls, ss)))
            | (contra_ls as _ :: _, co_ls) =>
              let
                val proofs =