# HG changeset patch
# User wenzelm
# Date 954763239 -7200
# Node ID 5427f450e9dae5641dd65d21015150ecae09b00a
# Parent  e5048a26e1d8d732b793e5d876ce97975188c470
markup_env_command 'text' / 'txt';

diff -r e5048a26e1d8 -r 5427f450e9da src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Apr 03 14:00:16 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 03 14:00:39 2000 +0200
@@ -51,7 +51,7 @@
   OuterSyntax.markup_command "subsubsection" "subsubsection heading" K.thy_heading
     (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
 
-val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
+val textP = OuterSyntax.markup_env_command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
 
 val text_rawP = OuterSyntax.verbatim_command "text_raw" "raw document preparation text"
@@ -67,7 +67,7 @@
 val subsubsectP = OuterSyntax.markup_command "subsubsect" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
 
-val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
+val txtP = OuterSyntax.markup_env_command "txt" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
 
 val txt_rawP = OuterSyntax.verbatim_command "txt_raw" "raw document preparation text (proof)"