filtering out some package theorems
authorpaulson
Fri Oct 05 09:59:03 2007 +0200 (2007-10-05)
changeset 248540ebcd575d3c6
parent 24853 aab5798e5a33
child 24855 161eb8381b49
filtering out some package theorems
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 05 08:38:09 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 05 09:59:03 2007 +0200
     1.3 @@ -606,12 +606,9 @@
     1.4    | add_single_names ((a, [th]), pairs) = (a,th)::pairs
     1.5    | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
     1.6  
     1.7 -val multi_base_blacklist =
     1.8 -  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
     1.9 -
    1.10  (*Ignore blacklisted basenames*)
    1.11  fun add_multi_names ((a, ths), pairs) =
    1.12 -  if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
    1.13 +  if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
    1.14    else add_single_names ((a, ths), pairs);
    1.15  
    1.16  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Oct 05 08:38:09 2007 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Oct 05 09:59:03 2007 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4    val cnf_axiom: thm -> thm list
     2.5    val meta_cnf_axiom: thm -> thm list
     2.6    val pairname: thm -> string * thm
     2.7 +  val multi_base_blacklist: string list 
     2.8    val skolem_thm: thm -> thm list
     2.9    val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
    2.10    val cnf_rules_of_ths: thm list -> thm list
    2.11 @@ -449,11 +450,18 @@
    2.12  fun too_complex t = 
    2.13    Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
    2.14    
    2.15 +val multi_base_blacklist =
    2.16 +  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
    2.17 +
    2.18  fun skolem_cache th thy =
    2.19    if PureThy.is_internal th orelse too_complex (prop_of th) then thy
    2.20    else #2 (skolem_cache_thm th thy);
    2.21  
    2.22 -val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of;
    2.23 +fun skolem_cache_list (a,ths) thy =
    2.24 +  if (Sign.base_name a) mem_string multi_base_blacklist then thy
    2.25 +  else fold skolem_cache ths thy;
    2.26 +
    2.27 +val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of;
    2.28  fun skolem_cache_node thy = skolem_cache_theorems_of thy thy;
    2.29  fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy;
    2.30