src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33056 791a4655cae3
parent 32970 fbd2bb2489a8
child 33063 4d462963a7db
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 21 16:57:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 21 17:34:35 2009 +0200
     1.3 @@ -262,8 +262,7 @@
     1.4    in
     1.5      thy2
     1.6      |> Sign.add_path (space_implode "_" new_type_names)
     1.7 -    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
     1.8 -         [Nitpick_Const_Simps.add])]
     1.9 +    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
    1.10      ||> Sign.parent_path
    1.11      ||> Theory.checkpoint
    1.12      |-> (fn thms => pair (reccomb_names, flat thms))
    1.13 @@ -335,7 +334,7 @@
    1.14            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    1.15    in
    1.16      thy2
    1.17 -    |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
    1.18 +    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
    1.19         o Context.Theory
    1.20      |> Sign.parent_path
    1.21      |> store_thmss "cases" new_type_names case_thms