--- a/src/Pure/Pure.thy Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Pure.thy Thu Nov 06 11:44:41 2014 +0100
@@ -13,7 +13,6 @@
"identifier" "if" "imports" "in" "includes" "infix" "infixl"
"infixr" "is" "keywords" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
- and "theory" :: thy_begin % "theory"
and "header" :: heading
and "chapter" :: heading
and "section" :: heading
@@ -27,7 +26,7 @@
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
- and "SML_file" "ML_file" :: thy_load % "ML"
+ and "SML_file" :: thy_load % "ML"
and "SML_import" "SML_export" :: thy_decl % "ML"
and "ML" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)