# HG changeset patch
# User paulson
# Date 1121259948 -7200
# Node ID 12d00dab530172fc0a8476f13ee275d41bdcdae9
# Parent  51600bfac17680d708183217295ae95783a31872
tidied

diff -r 51600bfac176 -r 12d00dab5301 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Jul 13 14:56:00 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Jul 13 15:05:48 2005 +0200
@@ -645,13 +645,7 @@
 	cls_str :: (typ_clss 0 tfree_lits)
     end;
 
-fun clause_info cls =
-    let 
-	val cls_id = string_of_clauseID cls
-	val ax_name = string_of_axiomName cls
-    in 
-	((ax_name^""), cls_id)
-    end;
+fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls);
 
 
 fun clause2tptp cls =