tuned;
authorwenzelm
Tue, 10 Jul 2007 23:29:52 +0200
changeset 23725 1f84af8b2e71
parent 23724 6e95ed5f64da
child 23726 2ebecff57b17
tuned;
src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jul 10 23:29:51 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jul 10 23:29:52 2007 +0200
@@ -344,7 +344,7 @@
       >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
 
     val other = Scan.peek (fn d =>
-       Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
+       P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
 
     val token =
       ignored ||