57 | _ => con; |
57 | _ => con; |
58 fun dis_name con = "is_"^ (extern_name con); |
58 fun dis_name con = "is_"^ (extern_name con); |
59 fun dis_name_ con = "is_"^ (strip_esc con); |
59 fun dis_name_ con = "is_"^ (strip_esc con); |
60 |
60 |
61 (* make distinct names out of the type list, |
61 (* make distinct names out of the type list, |
62 forbidding "o", "x..","f..","P.." as names *) |
62 forbidding "o","n..","x..","f..","P.." as names *) |
63 (* a number string is added if necessary *) |
63 (* a number string is added if necessary *) |
64 fun mk_var_names ids : string list = let |
64 fun mk_var_names ids : string list = let |
65 fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s; |
65 fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; |
66 fun index_vnames(vn::vns,occupied) = |
66 fun index_vnames(vn::vns,occupied) = |
67 (case assoc(occupied,vn) of |
67 (case assoc(occupied,vn) of |
68 None => if vn mem vns |
68 None => if vn mem vns |
69 then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) |
69 then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) |
70 else vn :: index_vnames(vns, occupied) |
70 else vn :: index_vnames(vns, occupied) |