# HG changeset patch
# User wenzelm
# Date 1464096272 -7200
# Node ID fd11a538daac7b2245d93eaad7bff94ccc2a0259
# Parent  035785035a1a63a2c31ac3755e27328e4ff63320
clarified syntax categories;

diff -r 035785035a1a -r fd11a538daac src/HOL/Tools/Nitpick/nitpick_commands.ML
--- 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
diff -r 035785035a1a -r fd11a538daac src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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)) []