# HG changeset patch
# User wenzelm
# Date 1256824675 -3600
# Node ID 4138ba02b6816113c7a92f0cc80f25422b0f5650
# Parent  a103fa7c19cc3add5673cc9d14b21479f7ffdb18
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
tuned;

diff -r a103fa7c19cc -r 4138ba02b681 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Oct 29 14:54:14 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML	Thu Oct 29 14:57:55 2009 +0100
@@ -352,7 +352,8 @@
 
 fun valid_facts facts =
   Facts.fold_static (fn (name, ths) =>
-    if run_blacklist_filter andalso is_package_def name then I
+    if Facts.is_concealed facts name orelse
+      (run_blacklist_filter andalso is_package_def name) then I
     else
       let val xname = Facts.extern facts name in
         if Name_Space.is_hidden xname then I
@@ -381,7 +382,7 @@
 
 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
 fun name_thm_pairs ctxt =
-  let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
+  let val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
       val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
       fun blacklisted x = run_blacklist_filter andalso is_some (Polyhash.peek ht x)
   in
@@ -499,17 +500,14 @@
     | Fol => true
     | Hol => false
 
-fun ths_to_cls thy ths =
-  ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname ths))
-
 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
     val isFO = isFO thy goal_cls
-    val included_thms = get_all_lemmas ctxt
-    val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
-                                     |> restrict_to_logic thy isFO
-                                     |> remove_unwanted_clauses
+    val included_cls = get_all_lemmas ctxt
+      |> ResAxioms.cnf_rules_pairs thy |> make_unique
+      |> restrict_to_logic thy isFO
+      |> remove_unwanted_clauses
   in
     relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) 
   end;
@@ -519,7 +517,8 @@
 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
     (* add chain thms *)
-    val chain_cls = ths_to_cls thy chain_ths
+    val chain_cls =
+      ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname chain_ths))
     val axcls = chain_cls @ axcls
     val extra_cls = chain_cls @ extra_cls
     val isFO = isFO thy goal_cls
diff -r a103fa7c19cc -r 4138ba02b681 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Oct 29 14:54:14 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 29 14:57:55 2009 +0100
@@ -316,18 +316,17 @@
 
 fun is_strange_thm th =
   case head_of (concl_of th) of
-      Const (a,_) => (a <> "Trueprop" andalso a <> "==")
+      Const (a, _) => (a <> "Trueprop" andalso a <> "==")
     | _ => false;
 
 fun bad_for_atp th =
-  Thm.is_internal th
-  orelse too_complex (prop_of th)
+  too_complex (prop_of th)
   orelse exists_type type_has_empty_sort (prop_of th)
   orelse is_strange_thm th;
 
 val multi_base_blacklist =
   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
-   "cases","ext_cases"];  (*FIXME: put other record thms here, or use the "Internal" marker*)
+   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "noatp" *)
 
 (*Keep the full complexity of the original name*)
 fun flatten_name s = space_implode "_X" (Long_Name.explode s);
@@ -421,8 +420,10 @@
 
 fun saturate_skolem_cache thy =
   let
-    val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
-      if already_seen thy name then I else cons (name, ths));
+    val facts = PureThy.facts_of thy;
+    val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
+      if Facts.is_concealed facts name orelse already_seen thy name then I
+      else cons (name, ths));
     val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
       if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
       else fold_index (fn (i, th) =>