src/HOL/Tools/res_atp.ML

   val tvar_classes_of_terms : term list -> string list
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
   val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
     (thm * (string * int)) list
-  val prepare_clauses : bool -> thm list ->
+  val prepare_clauses : bool -> thm list -> thm list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
     ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
     ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
 end;
 

   | check_named (_,th) = true;
 
 fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
 
 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
-fun get_clasimp_atp_lemmas ctxt user_thms =
+fun get_clasimp_atp_lemmas ctxt =
   let val included_thms =
-        if include_all
-        then (tap (fn ths => Output.debug
-                     (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
-                  (name_thm_pairs ctxt))
-        else
-        let val atpset_thms =
-                if include_atpset then ResAxioms.atpset_rules_of ctxt
-                else []
-            val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
-        in  atpset_thms  end
-      val user_rules = filter check_named
-                         (map ResAxioms.pairname
-                           (if null user_thms then whitelist else user_thms))
-  in
-      (filter check_named included_thms, user_rules)
+    if include_all
+    then (tap (fn ths => Output.debug
+                 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
+              (name_thm_pairs ctxt))
+    else
+    let val atpset_thms =
+            if include_atpset then ResAxioms.atpset_rules_of ctxt
+            else []
+        val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
+    in  atpset_thms  end
+  in
+    filter check_named included_thms
   end;
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
 (***************************************************************)

     | Hol => false
 
 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
-    val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
+    val included_thms = get_clasimp_atp_lemmas ctxt
     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
                                      |> restrict_to_logic thy (isFO thy goal_cls)
                                      |> remove_unwanted_clauses
+  in
+    relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+  end;
+
+(* prepare and count clauses before writing *)
+fun prepare_clauses dfg goal_cls chain_ths axcls thy =
+  let
+    val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
     val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
-    (*clauses relevant to goal gl*)
-  in
-    white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
-  end;
-
-(* prepare and count clauses before writing *)
-fun prepare_clauses dfg goal_cls axcls thy =
-  let
+    val axcls = white_cls @ axcls
     val ccls = subtract_cls goal_cls axcls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
     val ccltms = map prop_of ccls
     and axtms = map (prop_of o #1) axcls
     val subs = tfree_classes_of_terms ccltms