src/Pure/Thy/thy_output.ML
changeset 27732 8dbf5761a24a
parent 27566 6b20092af078
child 27755 f7cdde18aeb3
--- a/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -363,12 +363,11 @@
 
     (* spans *)
 
-    val stopper =
-      ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
-        fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
+    val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
+    val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
 
     val cmd = Scan.one (is_some o fst);
-    val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
+    val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
 
     val comments = Scan.many (comment_token o fst o snd);
     val blank = Scan.one (blank_token o fst o snd);