# HG changeset patch
# User mengj
# Date 1132294134 -3600
# Node ID d236379ea408850c64440678c9e61b877cd95c84
# Parent  95330fc0ea8defe83a705fc683b3d884fbc612cb
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.

diff -r 95330fc0ea8d -r d236379ea408 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Nov 18 07:08:18 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Nov 18 07:08:54 2005 +0100
@@ -548,9 +548,11 @@
     end;
 
 
-
+(* check if a clause is FOL first*)
 fun make_conjecture_clause n t =
-    let val (lits,types_sorts, preds, funcs) = literals_of_term t
+    let val _ = check_is_fol_term t
+	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
+	val (lits,types_sorts, preds, funcs) = literals_of_term t
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
         val tvars = get_tvar_strs types_sorts
     in
@@ -566,8 +568,11 @@
 val make_conjecture_clauses = make_conjecture_clauses_aux 0
 
 
+(*before converting an axiom clause to "clause" format, check if it is FOL*)
 fun make_axiom_clause term (ax_name,cls_id) =
-    let val (lits,types_sorts, preds,funcs) = literals_of_term term
+    let val _ = check_is_fol_term term 
+	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
+	val (lits,types_sorts, preds,funcs) = literals_of_term term
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
         val tvars = get_tvar_strs types_sorts	
     in