139 (InductivePackage.add_inductive_i false true big_rec_name false true false |
139 (InductivePackage.add_inductive_i false true big_rec_name false true false |
140 consts intr_ts [] []) thy1; |
140 consts intr_ts [] []) thy1; |
141 |
141 |
142 (********************************* typedef ********************************) |
142 (********************************* typedef ********************************) |
143 |
143 |
144 (* FIXME: quiet_mode flag for TypedefPackage and BREADTH_FIRST *) |
|
145 |
|
146 val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => |
144 val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => |
147 TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] [] |
145 setmp TypedefPackage.quiet_mode true |
148 (Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy) |
146 (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] [] |
149 (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~ |
147 (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1)))) thy) |
150 new_type_names)); |
148 (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~ |
|
149 new_type_names)); |
151 |
150 |
152 (*********************** definition of constructors ***********************) |
151 (*********************** definition of constructors ***********************) |
153 |
152 |
154 val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_"; |
153 val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_"; |
155 val rep_names = map (curry op ^ "Rep_") new_type_names; |
154 val rep_names = map (curry op ^ "Rep_") new_type_names; |