src/HOLCF/Tools/Domain/domain_library.ML
changeset 35443 2e0f9516947e
parent 35288 aa7da51ae1ef
child 35465 064bb6e9ace0
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Wed Feb 24 14:13:15 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Wed Feb 24 14:20:07 2010 -0800
@@ -162,7 +162,6 @@
   val dis_name : string -> string;
   val mat_name : string -> string;
   val pat_name : string -> string;
-  val mk_var_names : string list -> string list;
 end;
 
 structure Domain_Library :> DOMAIN_LIBRARY =
@@ -191,22 +190,6 @@
 fun pat_name  con = (extern_name con) ^ "_pat";
 fun pat_name_ con = (strip_esc   con) ^ "_pat";
 
-(* make distinct names out of the type list, 
-                                       forbidding "o","n..","x..","f..","P.." as names *)
-(* a number string is added if necessary *)
-fun mk_var_names ids : string list =
-    let
-      fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
-      fun index_vnames(vn::vns,occupied) =
-          (case AList.lookup (op =) occupied vn of
-             NONE => if vn mem vns
-                     then (vn^"1") :: index_vnames(vns,(vn,1)  ::occupied)
-                     else  vn      :: index_vnames(vns,          occupied)
-           | SOME(i) => (vn^(string_of_int (i+1)))
-                        :: index_vnames(vns,(vn,i+1)::occupied))
-        | index_vnames([],occupied) = [];
-    in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
-
 fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;