src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33459 a4a38ed813f7
parent 33338 de76079f973a
child 33643 b275f26a638b
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 05 22:59:57 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 05 23:59:23 2009 +0100
     1.3 @@ -338,8 +338,7 @@
     1.4            (DatatypeProp.make_cases new_type_names descr sorts thy2)
     1.5    in
     1.6      thy2
     1.7 -    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
     1.8 -       o Context.Theory
     1.9 +    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
    1.10      |> Sign.parent_path
    1.11      |> store_thmss "cases" new_type_names case_thms
    1.12      |-> (fn thmss => pair (thmss, case_names))