equal
deleted
inserted
replaced
178 ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); |
178 ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); |
179 |
179 |
180 val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = |
180 val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = |
181 setmp InductivePackage.quiet_mode (!quiet_mode) |
181 setmp InductivePackage.quiet_mode (!quiet_mode) |
182 (InductivePackage.add_inductive_i false true big_rec_name false true false |
182 (InductivePackage.add_inductive_i false true big_rec_name false true false |
183 consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1; |
183 consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1; |
184 |
184 |
185 (********************************* typedef ********************************) |
185 (********************************* typedef ********************************) |
186 |
186 |
187 val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => |
187 val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => |
188 setmp TypedefPackage.quiet_mode true |
188 setmp TypedefPackage.quiet_mode true |