author | wenzelm |
Tue, 10 Jul 2007 23:29:52 +0200 | |
changeset 23725 | 1f84af8b2e71 |
parent 23724 | 6e95ed5f64da |
child 23726 | 2ebecff57b17 |
--- 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 ||