1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 12:16:24 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 13:37:37 2013 +0100
     1.3 @@ -685,13 +685,14 @@
     1.4            atp_proof |> map_filter dep_of_step |> make_refute_graph
     1.5          val axioms = axioms_of_refute_graph refute_graph conjs
     1.6          val tainted = tainted_atoms_of_refute_graph refute_graph conjs
     1.7 +        val is_clause_tainted = exists (member (op =) tainted)
     1.8          val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
     1.9          val steps =
    1.10            Symtab.empty
    1.11            |> fold (fn Definition_Step _ => I (* FIXME *)
    1.12                      | Inference_Step (name as (s, ss), role, t, rule, _) =>
    1.13                        Symtab.update_new (s, (rule,
    1.14 -                        t |> (if member (op = o apsnd fst) tainted s then
    1.15 +                        t |> (if is_clause_tainted [name] then
    1.16                                  s_maybe_not role
    1.17                                  #> fold exists_of (map Var (Term.add_vars t []))
    1.18                                else
    1.19 @@ -741,12 +742,12 @@
    1.20                      By_Metis (fold (add_fact_from_dependencies fact_names) gamma
    1.21                                     ([], []))
    1.22                    fun prove outer = Prove (maybe_show outer c [], l, t, by)
    1.23 -                  val redirected = exists (member (op =) tainted) c
    1.24                  in
    1.25 -                  if redirected then
    1.26 +                  if is_clause_tainted c then
    1.27                      case gamma of
    1.28                        [g] =>
    1.29 -                      if is_clause_skolemize_rule g then
    1.30 +                      if is_clause_skolemize_rule g andalso
    1.31 +                         is_clause_tainted g then
    1.32                          let
    1.33                            val proof =
    1.34                              Fix (skolems_of (prop_of_clause g)) :: rev accum