src/Pure/Isar/isar_syn.ML
changeset 6890 05732285677e
parent 6888 d0c68ebdabc5
child 6904 4125d6b6d8f9
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jul 03 00:21:35 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 03 00:22:53 1999 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  (** formal comments **)
     1.5  
     1.6  val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
     1.7 -  (P.comment >> (Toplevel.proof o IsarThy.add_txt));
     1.8 +  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
     1.9  
    1.10  val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
    1.11    (P.comment >> (Toplevel.theory o IsarThy.add_text));