changeset 21895 | 6cbc0f69a21c |
parent 21882 | 04d8633fbd2f |
child 21911 | e29bcab0c81c |
--- 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 *)