src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Thu Mar 14 16:35:58 2019 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 14 16:55:06 2019 +0100
@@ -7,7 +7,7 @@
 
 theory Product_Type
   imports Typedef Inductive Fun
-  keywords "inductive_set" "coinductive_set" :: thy_decl
+  keywords "inductive_set" "coinductive_set" :: thy_defn
 begin
 
 subsection \<open>\<^typ>\<open>bool\<close> is a datatype\<close>