1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 06 22:41:35 2011 -0700
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 09:10:41 2011 +0200
     1.3 @@ -151,10 +151,12 @@
     1.4             error ("Unknown parameter: " ^ quote name ^ "."))
     1.5  
     1.6  
     1.7 -(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
     1.8 +(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
     1.9     handled correctly. *)
    1.10  fun implode_param [s, "?"] = s ^ "?"
    1.11 +  | implode_param [s, "??"] = s ^ "??"
    1.12    | implode_param [s, "!"] = s ^ "!"
    1.13 +  | implode_param [s, "!!"] = s ^ "!!"
    1.14    | implode_param ss = space_implode " " ss
    1.15  
    1.16  structure Data = Theory_Data
    1.17 @@ -376,12 +378,11 @@
    1.18                                         |> sort_strings |> cat_lines))
    1.19                    end))
    1.20  
    1.21 +val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
    1.22  val parse_key =
    1.23 -  Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
    1.24 -  >> implode_param
    1.25 +  Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
    1.26  val parse_value =
    1.27 -  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
    1.28 -                || Parse.$$$ "!")
    1.29 +  Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
    1.30  val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
    1.31  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
    1.32  val parse_fact_refs =