src/Pure/Thy/thy_output.ML
changeset 23725 1f84af8b2e71
parent 23272 25c84ca5e9a9
child 23863 8f3099589cfa
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jul 10 23:29:51 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jul 10 23:29:52 2007 +0200
     1.3 @@ -344,7 +344,7 @@
     1.4        >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
     1.5  
     1.6      val other = Scan.peek (fn d =>
     1.7 -       Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
     1.8 +       P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
     1.9  
    1.10      val token =
    1.11        ignored ||