diff -r aae5566d6756 -r 94aa7b81bcf6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -396,12 +396,12 @@
                                        |> sort_strings |> cat_lines))
                   end))
 
-val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
+val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
 val parse_key =
   Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
 val parse_value =
   Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
-val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)