1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Mar 07 16:47:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Mar 07 16:49:12 2006 +0100
     1.3 @@ -371,13 +371,10 @@
     1.4  fun list_ord _ ([],[]) = EQUAL
     1.5    | list_ord _ ([],_) = LESS
     1.6    | list_ord _ (_,[]) = GREATER
     1.7 -  | list_ord ord (x::xs, y::ys) =
     1.8 -    let val xy_ord = ord(x,y)
     1.9 -    in
    1.10 -	case xy_ord of EQUAL => list_ord ord (xs,ys)
    1.11 -		     | _ => xy_ord
    1.12 -    end;
    1.13 -
    1.14 +  | list_ord ord (x::xs, y::ys) = 
    1.15 +      (case ord(x,y) of EQUAL => list_ord ord (xs,ys)
    1.16 +	 	      | xy_ord => xy_ord);
    1.17 +		     
    1.18  fun type_ord (AtomV(_),AtomV(_)) = EQUAL
    1.19    | type_ord (AtomV(_),_) = LESS
    1.20    | type_ord (AtomF(_),AtomV(_)) = GREATER
    1.21 @@ -386,11 +383,8 @@
    1.22    | type_ord (Comp(_,_),AtomV(_)) = GREATER
    1.23    | type_ord (Comp(_,_),AtomF(_)) = GREATER
    1.24    | type_ord (Comp(con1,args1),Comp(con2,args2)) = 
    1.25 -    let val con_ord = string_ord(con1,con2)
    1.26 -    in
    1.27 -	case con_ord of EQUAL => types_ord (args1,args2)
    1.28 -		      | _ => con_ord
    1.29 -    end
    1.30 +      (case string_ord(con1,con2) of EQUAL => types_ord (args1,args2)
    1.31 +		      | con_ord => con_ord)
    1.32  and
    1.33      types_ord ([],[]) = EQUAL
    1.34    | types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2);
    1.35 @@ -608,15 +602,17 @@
    1.36  
    1.37  (*before converting an axiom clause to "clause" format, check if it is FOL*)
    1.38  fun make_axiom_clause term (ax_name,cls_id) =
    1.39 -    let val _ = check_is_fol_term term 
    1.40 -	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
    1.41 -	val (lits,types_sorts) = literals_of_term term
    1.42 +    let val (lits,types_sorts) = literals_of_term term
    1.43      in 
    1.44 -	if forall too_general_lit lits then
    1.45 +	if not (Meson.is_fol_term term) then
    1.46 +	   (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); 
    1.47 +	    NONE)
    1.48 +	else if forall too_general_lit lits then
    1.49  	   (Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); 
    1.50  	    NONE)
    1.51  	else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts))
    1.52 -    end;
    1.53 +    end
    1.54 +    handle CLAUSE _ => NONE;
    1.55  
    1.56  
    1.57  fun make_axiom_clauses_terms [] = []
    1.58 @@ -932,6 +928,7 @@
    1.59  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.60  fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 
    1.61    let 
    1.62 +    val _ = Output.debug ("Preparing to write the DFG file " ^ filename)
    1.63      val conjectures = make_conjecture_clauses (map prop_of ths)
    1.64      val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
    1.65      val clss = conjectures @ axclauses
    1.66 @@ -1031,6 +1028,7 @@
    1.67  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.68  fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) =
    1.69    let
    1.70 +    val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
    1.71      val clss = make_conjecture_clauses terms
    1.72      val axclauses' = make_axiom_clauses_terms axclauses
    1.73      val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)