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