Added in another function clause_name_of.
authormengj
Mon, 27 Nov 2006 23:48:10 +0100
changeset 21564 519ee3129ee1
parent 21563 b4718f2c15f0
child 21565 bd28361f4c5b
Added in another function clause_name_of.
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);