equal
deleted
inserted
replaced
67 val new_type_names = map (Binding.name_of o fst) types_syntax; |
67 val new_type_names = map (Binding.name_of o fst) types_syntax; |
68 val big_name = space_implode "_" new_type_names; |
68 val big_name = space_implode "_" new_type_names; |
69 val thy1 = Sign.add_path big_name thy; |
69 val thy1 = Sign.add_path big_name thy; |
70 val big_rec_name = big_name ^ "_rep_set"; |
70 val big_rec_name = big_name ^ "_rep_set"; |
71 val rep_set_names' = |
71 val rep_set_names' = |
72 (if length descr' = 1 then [big_rec_name] |
72 if length descr' = 1 then [big_rec_name] |
73 else |
73 else map (prefix (big_rec_name ^ "_") o string_of_int) (1 upto (length descr')); |
74 (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) |
|
75 (1 upto (length descr')))); |
|
76 val rep_set_names = map (Sign.full_bname thy1) rep_set_names'; |
74 val rep_set_names = map (Sign.full_bname thy1) rep_set_names'; |
77 |
75 |
78 val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr); |
76 val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr); |
79 val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts; |
77 val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts; |
80 val branchTs = Datatype_Aux.get_branching_types descr' sorts; |
78 val branchTs = Datatype_Aux.get_branching_types descr' sorts; |