src/HOL/Quotient.thy

--- a/src/HOL/Quotient.thy	Thu Mar 14 16:35:58 2019 +0100
+++ b/src/HOL/Quotient.thy	Thu Mar 14 16:55:06 2019 +0100
@@ -8,8 +8,8 @@
 imports Lifting
 keywords
   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
-  "quotient_type" :: thy_goal and "/" and
-  "quotient_definition" :: thy_goal
+  "quotient_type" :: thy_goal_defn and "/" and
+  "quotient_definition" :: thy_goal_defn
 begin
 
 text \<open>