diff -r e97452d79102 -r a6047f511de7 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Jan 13 16:41:32 2016 +0100
+++ b/src/Pure/Pure.thy	Wed Jan 13 16:55:56 2016 +0100
@@ -17,7 +17,7 @@
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
   and "typedecl" "type_synonym" "nonterminal" "judgment"
-    "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
+    "consts" "syntax" "no_syntax" "translations" "no_translations"
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl