# HG changeset patch
# User mengj
# Date 1163285926 -3600
# Node ID 3556301c18cdeca4651e9c360d83aa5dc8acff5d
# Parent  bfcc24fc7c46d46f11aa46f6e198a5bdada25d5f
Added in is_fol_thms.

diff -r bfcc24fc7c46 -r 3556301c18cd src/HOL/Tools/res_atp.ML
--- 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                             *)
 (***************************************************************)