--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue May 24 15:16:57 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue May 24 15:24:32 2016 +0200
@@ -292,7 +292,7 @@
extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
o map (apsnd single)
-val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_key = Scan.repeat1 Parse.embedded >> space_implode " "
val parse_value =
Scan.repeats1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue May 24 15:16:57 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue May 24 15:24:32 2016 +0200
@@ -348,7 +348,7 @@
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
-val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
+val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param
val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang)
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []