# HG changeset patch
# User wenzelm
# Date 965690248 -7200
# Node ID e3981c1f769df7f3afb20023a846f876b2d22766
# Parent  f4bfb69ae94e71611b22884b10d4cf996ed53d67
prf_heading kind;

diff -r f4bfb69ae94e -r e3981c1f769d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 07 14:34:26 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 08 01:17:28 2000 +0200
@@ -60,14 +60,14 @@
   (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
 
 
-val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)" K.prf_decl
-  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
+val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
+  K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
 
 val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
-  K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
+  K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
 
 val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
-  "formal comment (proof)" K.prf_decl
+  "formal comment (proof)" K.prf_heading
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
 
 val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
diff -r f4bfb69ae94e -r e3981c1f769d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 07 14:34:26 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 08 01:17:28 2000 +0200
@@ -30,6 +30,7 @@
       val qed: string
       val qed_block: string
       val qed_global: string
+      val prf_heading: string
       val prf_goal: string
       val prf_block: string
       val prf_open: string
@@ -84,6 +85,7 @@
   val qed = "qed";
   val qed_block = "qed-block";
   val qed_global = "qed-global";
+  val prf_heading = "proof-heading";
   val prf_goal = "proof-goal";
   val prf_block = "proof-block";
   val prf_open = "proof-open";
@@ -95,8 +97,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_open, prf_close, prf_chain, prf_decl,
-    prf_asm, prf_asm_goal, prf_script];
+    qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, prf_chain,
+    prf_decl, prf_asm, prf_asm_goal, prf_script];
 end;