# HG changeset patch
# User blanchet
# Date 1355345309 -3600
# Node ID 8825c36cb1cebcfe4e08708fccac3229bc5c8a46
# Parent  7e4f2f8d9b50924d62501d2b4627feaccc1dd29a
don't query blacklisted theorems in evaluation driver

diff -r 7e4f2f8d9b50 -r 8825c36cb1ce src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Dec 12 21:48:29 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Wed Dec 12 21:48:29 2012 +0100
@@ -129,6 +129,7 @@
 
 fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
   let
+    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts = all_facts ctxt
@@ -146,7 +147,12 @@
           escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
           encode_features feats
         val query =
-          if kind = "" orelse null deps then "" else "? " ^ core ^ "\n"
+          if kind = "" orelse null deps orelse
+             is_blacklisted_or_something ctxt ho_atp name orelse
+             Sledgehammer_Fact.is_bad_for_atps ho_atp th then
+            ""
+          else
+            "? " ^ core ^ "\n"
         val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
         val _ = File.append path (query ^ update)
       in [name] end
diff -r 7e4f2f8d9b50 -r 8825c36cb1ce src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
@@ -25,8 +25,7 @@
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   val backquote_thm : Proof.context -> thm -> string
   val is_bad_for_atps : bool -> thm -> bool
-  val is_concealed_or_backlisted_or_something :
-    Proof.context -> bool -> Facts.T -> string -> bool
+  val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   val build_all_names :
     (thm -> string) -> ('a * thm) list -> string Symtab.table
@@ -242,9 +241,7 @@
     exists_low_level_class_const t orelse is_that_fact th
   end
 
-fun is_concealed_or_backlisted_or_something ctxt ho_atp facts name =
-  Facts.is_concealed facts name orelse
-  not (can (Proof_Context.get_thms ctxt) name) orelse
+fun is_blacklisted_or_something ctxt ho_atp name =
   (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
 
@@ -431,7 +428,9 @@
         if not really_all andalso
            name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
-           is_concealed_or_backlisted_or_something ctxt ho_atp facts name0 then
+           (Facts.is_concealed facts name0 orelse
+            not (can (Proof_Context.get_thms ctxt) name0) orelse
+            is_blacklisted_or_something ctxt ho_atp name0) then
           I
         else
           let