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