1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Nov 18 07:08:18 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Nov 18 07:08:54 2005 +0100
     1.3 @@ -548,9 +548,11 @@
     1.4      end;
     1.5  
     1.6  
     1.7 -
     1.8 +(* check if a clause is FOL first*)
     1.9  fun make_conjecture_clause n t =
    1.10 -    let val (lits,types_sorts, preds, funcs) = literals_of_term t
    1.11 +    let val _ = check_is_fol_term t
    1.12 +	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
    1.13 +	val (lits,types_sorts, preds, funcs) = literals_of_term t
    1.14  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
    1.15          val tvars = get_tvar_strs types_sorts
    1.16      in
    1.17 @@ -566,8 +568,11 @@
    1.18  val make_conjecture_clauses = make_conjecture_clauses_aux 0
    1.19  
    1.20  
    1.21 +(*before converting an axiom clause to "clause" format, check if it is FOL*)
    1.22  fun make_axiom_clause term (ax_name,cls_id) =
    1.23 -    let val (lits,types_sorts, preds,funcs) = literals_of_term term
    1.24 +    let val _ = check_is_fol_term term 
    1.25 +	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
    1.26 +	val (lits,types_sorts, preds,funcs) = literals_of_term term
    1.27  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
    1.28          val tvars = get_tvar_strs types_sorts	
    1.29      in