src/HOL/Tools/res_clause.ML
changeset 21564 519ee3129ee1
parent 21560 d92389321fa7
child 21790 9d2761d09d91
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Nov 27 23:47:42 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Nov 27 23:48:10 2006 +0100
     1.3 @@ -654,6 +654,9 @@
     1.4  fun string_of_clausename (cls_id,ax_name) = 
     1.5      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
     1.6  
     1.7 +fun clause_name_of (cls_id,ax_name) = 
     1.8 +    ascii_of ax_name ^ "_" ^ Int.toString cls_id;
     1.9 +
    1.10  fun string_of_type_clsname (cls_id,ax_name,idx) = 
    1.11      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
    1.12