author | paulson |
Wed, 13 Jul 2005 15:05:48 +0200 | |
changeset 16794 | 12d00dab5301 |
parent 16793 | 51600bfac176 |
child 16795 | b400b53d8f7d |
--- 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 =