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