1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:15 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:17 2008 +0200
     1.3 @@ -363,12 +363,11 @@
     1.4  
     1.5      (* spans *)
     1.6  
     1.7 -    val stopper =
     1.8 -      ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
     1.9 -        fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
    1.10 +    val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
    1.11 +    val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
    1.12  
    1.13      val cmd = Scan.one (is_some o fst);
    1.14 -    val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
    1.15 +    val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
    1.16  
    1.17      val comments = Scan.many (comment_token o fst o snd);
    1.18      val blank = Scan.one (blank_token o fst o snd);