# HG changeset patch
# User paulson
# Date 1141746552 -3600
# Node ID 33f1b4515ce4fa89891238a73f76855ef2d40f62
# Parent  79053aa24abfc0a5e37760a67040e990591585c1
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.

diff -r 79053aa24abf -r 33f1b4515ce4 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Mar 07 16:47:51 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Tue Mar 07 16:49:12 2006 +0100
@@ -371,13 +371,10 @@
 fun list_ord _ ([],[]) = EQUAL
   | list_ord _ ([],_) = LESS
   | list_ord _ (_,[]) = GREATER
-  | list_ord ord (x::xs, y::ys) =
-    let val xy_ord = ord(x,y)
-    in
-	case xy_ord of EQUAL => list_ord ord (xs,ys)
-		     | _ => xy_ord
-    end;
-
+  | list_ord ord (x::xs, y::ys) = 
+      (case ord(x,y) of EQUAL => list_ord ord (xs,ys)
+	 	      | xy_ord => xy_ord);
+		     
 fun type_ord (AtomV(_),AtomV(_)) = EQUAL
   | type_ord (AtomV(_),_) = LESS
   | type_ord (AtomF(_),AtomV(_)) = GREATER
@@ -386,11 +383,8 @@
   | type_ord (Comp(_,_),AtomV(_)) = GREATER
   | type_ord (Comp(_,_),AtomF(_)) = GREATER
   | type_ord (Comp(con1,args1),Comp(con2,args2)) = 
-    let val con_ord = string_ord(con1,con2)
-    in
-	case con_ord of EQUAL => types_ord (args1,args2)
-		      | _ => con_ord
-    end
+      (case string_ord(con1,con2) of EQUAL => types_ord (args1,args2)
+		      | con_ord => con_ord)
 and
     types_ord ([],[]) = EQUAL
   | types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2);
@@ -608,15 +602,17 @@
 
 (*before converting an axiom clause to "clause" format, check if it is FOL*)
 fun make_axiom_clause term (ax_name,cls_id) =
-    let val _ = check_is_fol_term term 
-	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
-	val (lits,types_sorts) = literals_of_term term
+    let val (lits,types_sorts) = literals_of_term term
     in 
-	if forall too_general_lit lits then
+	if not (Meson.is_fol_term term) then
+	   (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); 
+	    NONE)
+	else if forall too_general_lit lits then
 	   (Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); 
 	    NONE)
 	else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts))
-    end;
+    end
+    handle CLAUSE _ => NONE;
 
 
 fun make_axiom_clauses_terms [] = []
@@ -932,6 +928,7 @@
 (* write out a subgoal in DFG format to the file "xxxx_N"*)
 fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 
   let 
+    val _ = Output.debug ("Preparing to write the DFG file " ^ filename)
     val conjectures = make_conjecture_clauses (map prop_of ths)
     val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
     val clss = conjectures @ axclauses
@@ -1031,6 +1028,7 @@
 (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
 fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) =
   let
+    val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
     val clss = make_conjecture_clauses terms
     val axclauses' = make_axiom_clauses_terms axclauses
     val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)