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