diff -r ec3a22e62b54 -r cbb94074682b src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Sun Jun 23 21:16:06 2013 +0200 +++ b/src/Tools/Code/code_runtime.ML Sun Jun 23 21:16:06 2013 +0200 @@ -357,10 +357,10 @@ val _ = Outer_Syntax.command @{command_spec "code_reflect"} "enrich runtime environment with generated code" - (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype + (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) [] - -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) [] - -- Scan.option (@{keyword "file"} |-- Parse.name) + -- Scan.optional (@{keyword "functions"} |-- Parse.!!! (Scan.repeat1 Parse.name)) [] + -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name) >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));