src/Pure/Isar/isar_syn.ML

     (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
 
 val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
 
-val verbatimP = OuterSyntax.markup_command "verbatim" "verbatim document preparation text"
+val verbatimP = OuterSyntax.verbatim_command "verbatim" "verbatim document preparation text"
   K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_verbatim));
 
 
 val sectP = OuterSyntax.markup_command "sect" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));

   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
 
 val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
 
-val verbP = OuterSyntax.markup_command "verb" "verbatim document preparation text (proof)"
+val verbP = OuterSyntax.verbatim_command "verb" "verbatim document preparation text (proof)"
   K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_verb)));
 
 
 
 (** theory sections **)