src/HOLCF/domain/interface.ML
changeset 1286 ae25649cbbb1
parent 1284 e5b95ee2616b
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
1285:4dd0651d692d 1286:ae25649cbbb1
    66 
    66 
    67 (* ----- generation of argument string for calling add_domain --------------------- *)
    67 (* ----- generation of argument string for calling add_domain --------------------- *)
    68 
    68 
    69 
    69 
    70      fun string_of_sort_emb [] = ""
    70      fun string_of_sort_emb [] = ""
    71      |   string_of_sort_emb [x] = x
    71      |   string_of_sort_emb [x] = "\"" ^x^ "\"" 
    72 	|   string_of_sort_emb (x::xs) = x^","^(string_of_sort_emb xs);
    72 	|   string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs);
    73 
    73 
    74 	fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
    74 	fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
    75 
    75 
    76     fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
    76     fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
    77     and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)
    77     and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)