# HG changeset patch
# User blanchet
# Date 1277396535 -7200
# Node ID 2e733b0a963ce59478294fb740ce07dfd61433ff
# Parent  8db1e5d4b93f9564b0e0e6df3299835556a53e79
a76ace919f1c wasn't quite right; second try

diff -r 8db1e5d4b93f -r 2e733b0a963c src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 18:04:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 18:22:15 2010 +0200
@@ -406,6 +406,9 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
 
+val exists_sledgehammer_const =
+  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
+
 fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
@@ -428,7 +431,8 @@
 
             val name1 = Facts.extern facts name;
             val name2 = Name_Space.extern full_space name;
-            val ths = filter_out is_theorem_bad_for_atps ths0;
+            val ths = filter_out (is_theorem_bad_for_atps orf
+                                  exists_sledgehammer_const) ths0
           in
             case find_first check_thms [name1, name2, name] of
               NONE => I
diff -r 8db1e5d4b93f -r 2e733b0a963c src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 18:04:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 18:22:15 2010 +0200
@@ -8,6 +8,8 @@
 signature SLEDGEHAMMER_FACT_PREPROCESSOR =
 sig
   type cnf_thm = thm * ((string * int) * thm)
+
+  val sledgehammer_prefix: string
   val chained_prefix: string
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
@@ -384,8 +386,6 @@
 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