1.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Oct 30 15:13:48 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 30 15:28:53 2007 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val cnf_axiom: thm -> thm list
     1.5    val pairname: thm -> string * thm
     1.6    val multi_base_blacklist: string list 
     1.7 +  val bad_for_atp: thm -> bool
     1.8    val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
     1.9    val cnf_rules_of_ths: thm list -> thm list
    1.10    val neg_clausify: thm list -> thm list
    1.11 @@ -320,6 +321,14 @@
    1.12  fun too_complex t = 
    1.13    Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
    1.14    
    1.15 +fun is_strange_thm th =
    1.16 +  case head_of (concl_of th) of
    1.17 +      Const (a,_) => (a <> "Trueprop" andalso a <> "==")
    1.18 +    | _ => false;
    1.19 +
    1.20 +fun bad_for_atp th = 
    1.21 +  PureThy.is_internal th orelse too_complex (prop_of th) orelse is_strange_thm th;
    1.22 +
    1.23  val multi_base_blacklist =
    1.24    ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
    1.25  
    1.26 @@ -381,8 +390,7 @@
    1.27  
    1.28  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    1.29  fun skolem_thm (s,th) =
    1.30 -  if (Sign.base_name s) mem_string multi_base_blacklist orelse 
    1.31 -     PureThy.is_internal th orelse too_complex (prop_of th) then []
    1.32 +  if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then []
    1.33    else 
    1.34        let val ctxt0 = Variable.thm_context th
    1.35  	  val (nnfth,ctxt1) = to_nnf th ctxt0
    1.36 @@ -450,8 +458,7 @@
    1.37  val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
    1.38  
    1.39  fun skolem_cache th thy =
    1.40 -  if PureThy.is_internal th orelse too_complex (prop_of th) then thy
    1.41 -  else #2 (skolem_cache_thm th thy);
    1.42 +  if bad_for_atp th then thy else #2 (skolem_cache_thm th thy);
    1.43  
    1.44  fun skolem_cache_list (a,ths) thy =
    1.45    if (Sign.base_name a) mem_string multi_base_blacklist then thy