src/HOL/Tools/res_clause.ML
changeset 21564 519ee3129ee1
parent 21560 d92389321fa7
child 21790 9d2761d09d91
equal deleted inserted replaced
21563:b4718f2c15f0 21564:519ee3129ee1
   652       in  name ^ (paren_pack (map string_of_term ts @ typs'))  end;
   652       in  name ^ (paren_pack (map string_of_term ts @ typs'))  end;
   653 
   653 
   654 fun string_of_clausename (cls_id,ax_name) = 
   654 fun string_of_clausename (cls_id,ax_name) = 
   655     clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   655     clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   656 
   656 
       
   657 fun clause_name_of (cls_id,ax_name) = 
       
   658     ascii_of ax_name ^ "_" ^ Int.toString cls_id;
       
   659 
   657 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   660 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   658     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   661     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   659 
   662 
   660 (*Write a list of strings to a file*)
   663 (*Write a list of strings to a file*)
   661 fun writeln_strs os = List.app (fn s => TextIO.output (os,s));
   664 fun writeln_strs os = List.app (fn s => TextIO.output (os,s));