--- a/src/Pure/Pure.thy Thu Feb 28 16:19:08 2013 +0100
+++ b/src/Pure/Pure.thy Thu Feb 28 16:38:17 2013 +0100
@@ -25,7 +25,7 @@
and "txt" "txt_raw" :: prf_decl % "proof"
and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
"nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
- "translations" "no_translations" "axioms" "defs" "definition"
+ "translations" "no_translations" "defs" "definition"
"abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl