--- a/src/Pure/Pure.thy Fri Jul 04 14:58:52 2014 +0200
+++ b/src/Pure/Pure.thy Fri Jul 04 15:46:13 2014 +0200
@@ -24,7 +24,8 @@
and "subsect" :: prf_heading3 % "proof"
and "subsubsect" :: prf_heading4 % "proof"
and "txt" "txt_raw" :: prf_decl % "proof"
- and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment"
+ and "default_sort" :: thy_decl == ""
+ and "typedecl" "type_synonym" "nonterminal" "judgment"
"consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"