Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dont skolemize conjecture
authorsmolkas
Thu, 14 Feb 2013 22:49:22 +0100
changeset 51129 1edc2cc25f19
parent 51128 0021ea861129
child 51130 76d68444cd59
dont skolemize conjecture
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle