src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 31902 862ae16a799d
parent 31775 2b04504fcb69
child 32124 954321008785
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4      thy2
     1.5      |> Sign.add_path (space_implode "_" new_type_names)
     1.6      |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
     1.7 -         [Nitpick_Const_Simp_Thms.add])]
     1.8 +         [Nitpick_Const_Simps.add])]
     1.9      ||> Sign.parent_path
    1.10      ||> Theory.checkpoint
    1.11      |-> (fn thms => pair (reccomb_names, Library.flat thms))
    1.12 @@ -337,7 +337,7 @@
    1.13            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    1.14    in
    1.15      thy2
    1.16 -    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
    1.17 +    |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
    1.18         o Context.Theory
    1.19      |> parent_path (#flat_names config)
    1.20      |> store_thmss "cases" new_type_names case_thms