--- a/src/Pure/Pure.thy Tue Jun 25 19:25:40 2013 +0200
+++ b/src/Pure/Pure.thy Tue Jun 25 20:35:50 2013 +0200
@@ -13,8 +13,8 @@
"identifier" "if" "imports" "in" "includes" "infix" "infixl"
"infixr" "is" "keywords" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
- and "theory" :: thy_begin
- and "ML_file" :: thy_load
+ and "theory" :: thy_begin % "theory"
+ and "ML_file" :: thy_load % "ML"
and "header" :: diag
and "chapter" :: thy_heading1
and "section" :: thy_heading2