diff -r 1a0e32ccb8bb -r 6cbc0f69a21c src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Thu Dec 21 13:55:14 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Thu Dec 21 13:55:15 2006 +0100
@@ -150,9 +150,9 @@
   end;
 
 fun parse_args f args =
-  case f args
-   of (x, []) => x
-    | (_, _) => error "bad serializer arguments";
+  case Scan.read Args.stopper f args
+   of SOME x => x
+    | NONE => error "bad serializer arguments";
 
 
 (* list and string serializer *)