src/Pure/Isar/isar_syn.ML
changeset 9552 e3981c1f769d
parent 9465 b285b91cd2b2
child 9589 95a66548c883
--- 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)"