# HG changeset patch # User blanchet # Date 1341871085 -7200 # Node ID 999d6a829c2873e0b7be1b0c177965e51d3bec3b # Parent 49930a9ec27ce526a7e8166c60719f6ad0e340bb compile diff -r 49930a9ec27c -r 999d6a829c28 src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Mon Jul 09 23:23:12 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Mon Jul 09 23:58:05 2012 +0200 @@ -5,7 +5,7 @@ header {* ATP Theory Exporter *} theory ATP_Theory_Export -imports "~~/src/HOL/Sledgehammer2d" Complex_Main (* ### *) +imports Complex_Main uses "atp_theory_export.ML" begin diff -r 49930a9ec27c -r 999d6a829c28 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Mon Jul 09 23:23:12 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 09 23:58:05 2012 +0200 @@ -252,9 +252,10 @@ @{thm Bex_def}, @{thm If_def}] fun is_likely_tautology thy th = - member Thm.eq_thm_prop known_tautologies th orelse - th |> prop_of |> raw_interesting_const_names thy - |> forall (is_skolem orf is_abs) + (member Thm.eq_thm_prop known_tautologies th orelse + th |> prop_of |> raw_interesting_const_names thy + |> forall (is_skolem orf is_abs)) andalso + not (Thm.eq_thm_prop (@{thm ext}, th)) fun generate_mash_dependency_file_for_theory thy include_thy file_name = let