equal
deleted
inserted
replaced
10 fun nth_dtyp dt_descr sorts i = |
10 fun nth_dtyp dt_descr sorts i = |
11 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
11 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
12 *} |
12 *} |
13 |
13 |
14 ML {* |
14 ML {* |
15 (* generates for every datatype a name str ^ dt_name *) |
15 (* generates for every datatype a name str ^ dt_name |
|
16 plus and index for multiple occurences of a string *) |
16 fun prefix_dt_names dt_descr sorts str = |
17 fun prefix_dt_names dt_descr sorts str = |
17 let |
18 let |
18 fun get_nth_name (i, _) = |
19 fun get_nth_name (i, _) = |
19 Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) |
20 Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) |
20 in |
21 in |