| changeset 21564 | 519ee3129ee1 |
| parent 21560 | d92389321fa7 |
| child 21790 | 9d2761d09d91 |
--- 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);