# HG changeset patch
# User wenzelm
# Date 1184102992 -7200
# Node ID 1f84af8b2e719dafe744860a5ce7260c8aada97a
# Parent  6e95ed5f64da1497def54e83052450f08cf503cd
tuned;

diff -r 6e95ed5f64da -r 1f84af8b2e71 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 ||