src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Thu Mar 14 16:35:58 2019 +0100
+++ b/src/HOL/Fun.thy	Thu Mar 14 16:55:06 2019 +0100
@@ -8,7 +8,7 @@
 
 theory Fun
   imports Set
-  keywords "functor" :: thy_goal
+  keywords "functor" :: thy_goal_defn
 begin
 
 lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"