--- 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