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 =