--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Sun Oct 18 21:30:01 2015 +0200
@@ -294,11 +294,10 @@
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value =
- Scan.repeat1 (Parse.minus >> single
+ Scan.repeats1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus
(Parse.name || Parse.float_number))
|| @{keyword ","} |-- Parse.number >> prefix "," >> single)
- >> flat
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
val parse_params =
Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []