1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -396,12 +396,12 @@
     1.4                                         |> sort_strings |> cat_lines))
     1.5                    end))
     1.6  
     1.7 -val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
     1.8 +val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}
     1.9  val parse_key =
    1.10    Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
    1.11  val parse_value =
    1.12    Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
    1.13 -val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
    1.14 +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
    1.15  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
    1.16  val parse_fact_refs =
    1.17    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)