--- 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
--- 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