src/HOL/Library/Old_Recdef.thy
changeset 69913 ca515cf61651
parent 69605 a96320074298
child 82299 a0693649e9c6
--- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 14 16:35:58 2019 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 14 16:55:06 2019 +0100
@@ -7,7 +7,7 @@
 theory Old_Recdef
 imports Main
 keywords
-  "recdef" :: thy_decl and
+  "recdef" :: thy_defn and
   "permissive" "congs" "hints"
 begin