174 ((Rep_name ^ "_inverse", make Rep_inverse), []), |
174 ((Rep_name ^ "_inverse", make Rep_inverse), []), |
175 ((Abs_name ^ "_inverse", abs_inverse), []), |
175 ((Abs_name ^ "_inverse", abs_inverse), []), |
176 ((Rep_name ^ "_inject", make Rep_inject), []), |
176 ((Rep_name ^ "_inject", make Rep_inject), []), |
177 ((Abs_name ^ "_inject", abs_inject), []), |
177 ((Abs_name ^ "_inject", abs_inject), []), |
178 ((Rep_name ^ "_cases", make Rep_cases), |
178 ((Rep_name ^ "_cases", make Rep_cases), |
179 [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]), |
179 [RuleCases.case_names [Rep_name], Induct.cases_set full_name]), |
180 ((Abs_name ^ "_cases", make Abs_cases), |
180 ((Abs_name ^ "_cases", make Abs_cases), |
181 [RuleCases.case_names [Abs_name], InductAttrib.cases_type full_tname]), |
181 [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), |
182 ((Rep_name ^ "_induct", make Rep_induct), |
182 ((Rep_name ^ "_induct", make Rep_induct), |
183 [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]), |
183 [RuleCases.case_names [Rep_name], Induct.induct_set full_name]), |
184 ((Abs_name ^ "_induct", make Abs_induct), |
184 ((Abs_name ^ "_induct", make Abs_induct), |
185 [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])]) |
185 [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) |
186 ||> Sign.parent_path; |
186 ||> Sign.parent_path; |
187 val info = {rep_type = oldT, abs_type = newT, |
187 val info = {rep_type = oldT, abs_type = newT, |
188 Rep_name = full Rep_name, Abs_name = full Abs_name, |
188 Rep_name = full Rep_name, Abs_name = full Abs_name, |
189 type_definition = type_definition, set_def = set_def, |
189 type_definition = type_definition, set_def = set_def, |
190 Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |
190 Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |