src/HOL/BNF_Def.thy

--- a/src/HOL/BNF_Def.thy	Thu Mar 14 16:35:58 2019 +0100
+++ b/src/HOL/BNF_Def.thy	Thu Mar 14 16:55:06 2019 +0100
@@ -12,7 +12,7 @@
 imports BNF_Cardinal_Arithmetic Fun_Def_Base
 keywords
   "print_bnfs" :: diag and
-  "bnf" :: thy_goal
+  "bnf" :: thy_goal_defn
 begin
 
 lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"