1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 18:04:31 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 18:22:15 2010 +0200
     1.3 @@ -406,6 +406,9 @@
     1.4  fun subtract_cls ax_clauses =
     1.5    filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
     1.6  
     1.7 +val exists_sledgehammer_const =
     1.8 +  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
     1.9 +
    1.10  fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
    1.11    let
    1.12      val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
    1.13 @@ -428,7 +431,8 @@
    1.14  
    1.15              val name1 = Facts.extern facts name;
    1.16              val name2 = Name_Space.extern full_space name;
    1.17 -            val ths = filter_out is_theorem_bad_for_atps ths0;
    1.18 +            val ths = filter_out (is_theorem_bad_for_atps orf
    1.19 +                                  exists_sledgehammer_const) ths0
    1.20            in
    1.21              case find_first check_thms [name1, name2, name] of
    1.22                NONE => I