diff -r b4718f2c15f0 -r 519ee3129ee1 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Mon Nov 27 23:47:42 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Mon Nov 27 23:48:10 2006 +0100
@@ -654,6 +654,9 @@
 fun string_of_clausename (cls_id,ax_name) = 
     clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
 
+fun clause_name_of (cls_id,ax_name) = 
+    ascii_of ax_name ^ "_" ^ Int.toString cls_id;
+
 fun string_of_type_clsname (cls_id,ax_name,idx) = 
     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);