1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 10:48:06 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 11:27:15 2013 +0100
     1.3 @@ -720,12 +720,12 @@
     1.4                | _ => fold (curry s_disj) lits @{term False}
     1.5              end
     1.6              |> HOLogic.mk_Trueprop |> close_form
     1.7 -        fun maybe_show outer c =
     1.8 -          (outer andalso length c = 1 andalso subset (op =) (c, conjs))
     1.9 -          ? cons Show
    1.10 -        fun isar_proof_of_direct_proof _ accum [] = rev accum
    1.11 +        fun isar_proof_of_direct_proof _ accum [] = assms @ rev accum
    1.12            | isar_proof_of_direct_proof outer accum (inf :: infs) =
    1.13              let
    1.14 +              fun maybe_show outer c =
    1.15 +                (outer andalso length c = 1 andalso subset (op =) (c, conjs))
    1.16 +                ? cons Show
    1.17                fun do_rest step =
    1.18                  isar_proof_of_direct_proof outer (step :: accum) infs
    1.19                val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
    1.20 @@ -740,12 +740,30 @@
    1.21                    val by =
    1.22                      By_Metis (fold (add_fact_from_dependencies fact_names) gamma
    1.23                                     ([], []))
    1.24 +                  fun prove outer = Prove (maybe_show outer c [], l, t, by)
    1.25 +                  val redirected = exists (member (op =) tainted) c
    1.26                  in
    1.27 -                  if is_clause_skolemize_rule c andalso
    1.28 -                     not (member (op =) tainted (the_single c)) then
    1.29 -                    do_rest (Obtain ([], skolems_of t, l, t, by))
    1.30 +                  if redirected then
    1.31 +                    case gamma of
    1.32 +                      [g] =>
    1.33 +                      if is_clause_skolemize_rule g then
    1.34 +                        let
    1.35 +                          val proof =
    1.36 +                            Fix (skolems_of (prop_of_clause g)) :: rev accum
    1.37 +                        in
    1.38 +                          isar_proof_of_direct_proof outer
    1.39 +                              [Prove (maybe_show outer c [Then],
    1.40 +                                      label_of_clause c, prop_of_clause c,
    1.41 +                                      Subblock proof)] []
    1.42 +                        end
    1.43 +                      else
    1.44 +                        do_rest (prove outer)
    1.45 +                    | _ => do_rest (prove outer)
    1.46                    else
    1.47 -                    do_rest (Prove (maybe_show outer c [], l, t, by))
    1.48 +                    if is_clause_skolemize_rule c then
    1.49 +                      do_rest (Obtain ([], skolems_of t, l, t, by))
    1.50 +                    else
    1.51 +                      do_rest (prove outer)
    1.52                  end
    1.53                | Cases cases =>
    1.54                  let
    1.55 @@ -753,15 +771,16 @@
    1.56                      Assume (label_of_clause c, prop_of_clause c) ::
    1.57                      isar_proof_of_direct_proof false [] infs
    1.58                    val c = succedent_of_cases cases
    1.59 -                  val step =
    1.60 -                    Prove (maybe_show outer c [Ultimately], label_of_clause c,
    1.61 -                           prop_of_clause c, Case_Split (map do_case cases))
    1.62 -                in do_rest step end
    1.63 +                in
    1.64 +                  do_rest (Prove (maybe_show outer c [Ultimately],
    1.65 +                                  label_of_clause c, prop_of_clause c,
    1.66 +                                  Case_Split (map do_case cases)))
    1.67 +                end
    1.68              end
    1.69          val (isar_proof, (preplay_fail, preplay_time)) =
    1.70            refute_graph
    1.71            |> redirect_graph axioms tainted bot
    1.72 -          |> isar_proof_of_direct_proof true assms
    1.73 +          |> isar_proof_of_direct_proof true []
    1.74            |> (if not preplay andalso isar_compress <= 1.0 then
    1.75                  rpair (false, (true, seconds 0.0))
    1.76                else