# HG changeset patch
# User blanchet
# Date 1277395056 -7200
# Node ID a76ace919f1cba65b053b5b1fd2a1a83fa577c07
# Parent  48273d1ea331fb694cc9d46482127e03aa3f3991
never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts

diff -r 48273d1ea331 -r a76ace919f1c src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Jun 24 17:27:18 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Jun 24 17:57:36 2010 +0200
@@ -53,16 +53,6 @@
 lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
   by (simp add: fequal_def)
 
-text{*These two represent the equivalence between Boolean equality and iff.
-They can't be converted to clauses automatically, as the iff would be
-expanded...*}
-
-lemma iff_positive: "P \<or> Q \<or> P = Q"
-by blast
-
-lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
-by blast
-
 text{*Theorems for translation to combinators*}
 
 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
diff -r 48273d1ea331 -r a76ace919f1c src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:27:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:57:36 2010 +0200
@@ -35,13 +35,15 @@
 
 type cnf_thm = thm * ((string * int) * thm)
 
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
 (* Used to label theorems chained into the goal. *)
-val chained_prefix = "Sledgehammer.chained_"
+val chained_prefix = sledgehammer_prefix ^ "chained_"
 
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
-val skolem_theory_name = "Sledgehammer.Sko"
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
 val skolem_prefix = "sko_"
 val skolem_infix = "$"
 
@@ -382,6 +384,8 @@
 fun is_theorem_bad_for_atps thm =
   let val t = prop_of thm in
     is_formula_too_complex t orelse exists_type type_has_topsort t orelse
+    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s
+                   | _ => false) t orelse
     is_strange_thm thm
   end