1.1 --- a/src/HOL/Tools/res_atp.ML	Sun Jun 28 15:01:28 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sun Jun 28 15:01:28 2009 +0200
     1.3 @@ -296,7 +296,11 @@
     1.4  
     1.5  (*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
     1.6    or identified with ATPset (which however is too big currently)*)
     1.7 -val whitelist = [subsetI];
     1.8 +val whitelist_fo = [subsetI];
     1.9 +(* ext has been a 'helper clause', always given to the atps.
    1.10 +  As such it was not passed to metis, but metis does not include ext (in contrast
    1.11 +  to the other helper_clauses *)
    1.12 +val whitelist_ho = [ResHolClause.ext];
    1.13  
    1.14  (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
    1.15  
    1.16 @@ -531,8 +535,9 @@
    1.17     create additional clauses based on the information from extra_cls *)
    1.18  fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
    1.19    let
    1.20 -    val white_thms =
    1.21 -      filter check_named (map ResAxioms.pairname (whitelist @ chain_ths))
    1.22 +    val isFO = isFO thy goal_cls
    1.23 +    val white_thms = filter check_named (map ResAxioms.pairname
    1.24 +      (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths))
    1.25      val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
    1.26      val extra_cls = white_cls @ extra_cls
    1.27      val axcls = white_cls @ axcls
    1.28 @@ -546,7 +551,7 @@
    1.29      (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.30      val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
    1.31      val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
    1.32 -    val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
    1.33 +    val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
    1.34      val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
    1.35      val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
    1.36    in

     2.1 --- a/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
     2.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
     2.3 @@ -423,7 +423,7 @@
     2.4          val S = if needed "c_COMBS"
     2.5                  then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
     2.6                  else []
     2.7 -        val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
     2.8 +        val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
     2.9      in
    2.10          map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
    2.11      end;