tuned;
authorwenzelm
Tue Jul 10 23:29:52 2007 +0200 (2007-07-10)
changeset 237251f84af8b2e71
parent 23724 6e95ed5f64da
child 23726 2ebecff57b17
tuned;
src/Pure/Thy/thy_output.ML
     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 ||