prf_open/close;

--- a/src/Pure/Isar/isar_syn.ML	Wed Jun 07 17:14:58 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jun 08 21:53:44 2000 +0200
@@ -348,11 +348,11 @@
 (* proof structure *)
 
 val beginP =
-  OuterSyntax.command "{" "begin explicit proof block" K.prf_block
+  OuterSyntax.command "{" "begin explicit proof block" K.prf_open
     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block)));
 
 val endP =
-  OuterSyntax.command "}" "end explicit proof block" K.prf_block
+  OuterSyntax.command "}" "end explicit proof block" K.prf_close
     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block)));
 
 val nextP =

--- a/src/Pure/Isar/outer_syntax.ML	Wed Jun 07 17:14:58 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jun 08 21:53:44 2000 +0200
@@ -33,6 +33,8 @@
       val qed_global: string
       val prf_goal: string
       val prf_block: string
+      val prf_open: string
+      val prf_close: string
       val prf_chain: string
       val prf_decl: string
       val prf_asm: string
@@ -90,6 +92,8 @@
   val qed_global = "qed-global";
   val prf_goal = "proof-goal";
   val prf_block = "proof-block";
+  val prf_open = "proof-open";
+  val prf_close = "proof-close";
   val prf_chain = "proof-chain";
   val prf_decl = "proof-decl";
   val prf_asm = "proof-asm";
@@ -97,8 +101,8 @@
   val prf_script = "proof-script";
 
   val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
-    qed, qed_block, qed_global, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal,
-    prf_script];
+    qed, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
+    prf_asm, prf_asm_goal, prf_script];
 end;