# HG changeset patch
# User smolkas
# Date 1360878562 -3600
# Node ID 1edc2cc25f1988d914ed4a7fbbc31bd551b27e67
# Parent  0021ea86112905e0ed530d8f1e250b680d674e5e
dont skolemize conjecture

diff -r 0021ea861129 -r 1edc2cc25f19 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -699,7 +699,8 @@
                               else
                                 I))))
                   atp_proof
-        fun is_clause_skolemize_rule [(s, _)] =
+        fun is_clause_skolemize_rule [atom as (s, _)] =
+            not (member (op =) tainted atom) andalso
             Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
             SOME true
           | is_clause_skolemize_rule _ = false