equal
deleted
inserted
replaced
64 val big_rec_name = Sign.intern_const sign big_rec_base_name; |
64 val big_rec_name = Sign.intern_const sign big_rec_base_name; |
65 |
65 |
66 val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists); |
66 val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists); |
67 |
67 |
68 val dummy = |
68 val dummy = |
69 writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ big_rec_name); |
69 writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name); |
70 |
70 |
71 val case_varname = "f"; (*name for case variables*) |
71 val case_varname = "f"; (*name for case variables*) |
72 |
72 |
73 (** Define the constructors **) |
73 (** Define the constructors **) |
74 |
74 |