# HG changeset patch
# User wenzelm
# Date 1304189916 -7200
# Node ID 651aef3cc854c733652a226b0bba58c810098a0d
# Parent  876887b07e8df145a744f03a6fd7d5f81772edbd
tuned;

diff -r 876887b07e8d -r 651aef3cc854 src/Pure/Thy/rail.ML
--- a/src/Pure/Thy/rail.ML	Sat Apr 30 20:48:29 2011 +0200
+++ b/src/Pure/Thy/rail.ML	Sat Apr 30 20:58:36 2011 +0200
@@ -74,8 +74,7 @@
 
 in
 
-fun tokenize text =
-  #1 (Scan.error (Scan.finite Symbol_Pos.stopper scan) (Symbol_Pos.explode text));
+val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
 
 end;
 
@@ -175,10 +174,8 @@
 
 in
 
-fun read text =
-  (case Scan.error (Scan.finite stopper rules) (tokenize text) of
-    (res, []) => res
-  | (_, tok :: _) => error ("Malformed rail input: " ^ print tok));
+val read =
+  #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
 
 end;