--- a/src/HOL/Tools/res_atp_setup.ML Fri Feb 03 17:02:33 2006 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML Fri Feb 03 17:08:03 2006 +0100
@@ -291,7 +291,9 @@
(**** clausification ****)
fun cls_axiom_fol _ _ [] = []
| cls_axiom_fol name i (tm::tms) =
- (ResClause.make_axiom_clause tm (name,i)) :: (cls_axiom_fol name (i+1) tms);
+ case ResClause.make_axiom_clause tm (name,i) of
+ SOME cls => cls :: cls_axiom_fol name (i+1) tms
+ | NONE => cls_axiom_fol name i tms;
fun cls_axiom_hol _ _ [] = []
| cls_axiom_hol name i (tm::tms) =