diff -r 233f30abb040 -r a7bc1bdb8bb4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 06 22:41:35 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 09:10:41 2011 +0200
@@ -151,10 +151,12 @@
            error ("Unknown parameter: " ^ quote name ^ "."))
 
 
-(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
+(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
    handled correctly. *)
 fun implode_param [s, "?"] = s ^ "?"
+  | implode_param [s, "??"] = s ^ "??"
   | implode_param [s, "!"] = s ^ "!"
+  | implode_param [s, "!!"] = s ^ "!!"
   | implode_param ss = space_implode " " ss
 
 structure Data = Theory_Data
@@ -376,12 +378,11 @@
                                        |> sort_strings |> cat_lines))
                   end))
 
+val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
 val parse_key =
-  Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
-  >> implode_param
+  Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
 val parse_value =
-  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
-                || Parse.$$$ "!")
+  Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =