src/Pure/Isar/outer_syntax.ML

       val qed_block: string
       val prf_goal: string
       val prf_block: string
       val prf_chain: string
       val prf_decl: string
+      val prf_asm: string
       val prf_script: string
       val kinds: string list
     end
   type token
   type parser

   val qed_block = "qed-block";
   val prf_goal = "proof-goal";
   val prf_block = "proof-block";
   val prf_chain = "proof-chain";
   val prf_decl = "proof-decl";
+  val prf_asm = "proof-asm";
   val prf_script = "proof-script";
 
   val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
-    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_script];
+    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
 end;
 
 
 (* parsers *)