changeset 14799 | a405aadff16c |
parent 13641 | 63d1790a43ed |
child 14981 | e73f8140af78 |
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri May 21 21:47:07 2004 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri May 21 21:48:03 2004 +0200 @@ -339,8 +339,7 @@ (DatatypeProp.make_cases new_type_names descr sorts thy2) in - thy2 |> Theory.add_trrules_i - (DatatypeProp.make_case_trrules new_type_names descr) |> + thy2 |> parent_path flat_names |> store_thmss "cases" new_type_names case_thms |> apsnd (rpair case_names)