# 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