# HG changeset patch
# User wenzelm
# Date 1372185350 -7200
# Node ID 79e7fd57acc40a87d054863f8ca071b18e2d59d9
# Parent  082a1c8c2c89364d8649372dd4bfba875b75676c
recover command tags from 4cf3f6153eb8 -- important for document preparation;

diff -r 082a1c8c2c89 -r 79e7fd57acc4 src/Pure/Pure.thy
--- 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