# HG changeset patch
# User mengj
# Date 1164667690 -3600
# Node ID 519ee3129ee1f1ac822cb11eb97fbbae7fc4bbd4
# Parent  b4718f2c15f0ae28ae611f6303a0622f46aac2ac
Added in another function clause_name_of.

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);