# HG changeset patch
# User wenzelm
# Date 927751407 -7200
# Node ID 429bbd7ef26dd785ffe8a05c026cef2dba1a1b6c
# Parent  cf9f66ca9ee3898e15054c36d559fd2c9592df57
qed_block keywords;

diff -r cf9f66ca9ee3 -r 429bbd7ef26d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed May 26 16:51:05 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 26 22:43:27 1999 +0200
@@ -29,6 +29,7 @@
       val thy_decl: string
       val thy_goal: string
       val qed: string
+      val qed_block: string
       val prf_goal: string
       val prf_block: string
       val prf_chain: string
@@ -70,6 +71,7 @@
   val thy_decl = "theory-decl";
   val thy_goal = "theory-goal";
   val qed = "qed";
+  val qed_block = "qed-block";
   val prf_goal = "proof-goal";
   val prf_block = "proof-block";
   val prf_chain = "proof-chain";
@@ -77,7 +79,7 @@
   val prf_script = "proof-script";
 
   val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
-    prf_goal, prf_block, prf_chain, prf_decl, prf_script];
+    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_script];
 end;