Added in is_fol_thms.

--- a/src/HOL/Tools/res_atp.ML	Sat Nov 11 21:13:12 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Sat Nov 11 23:58:46 2006 +0100
@@ -51,6 +51,7 @@
   val rm_simpset : unit -> unit
   val rm_atpset : unit -> unit
   val rm_clasimp : unit -> unit
+  val is_fol_thms : thm list -> bool
 end;
 
 structure ResAtp =
@@ -304,6 +305,8 @@
     
 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
 
+fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
+
 (***************************************************************)
 (* Retrieving and filtering lemmas                             *)
 (***************************************************************)