1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
     1.5  struct
     1.6  
     1.7 +open ATP_Util
     1.8  open ATP_Systems
     1.9  open ATP_Translate
    1.10  open Sledgehammer_Util
    1.11 @@ -151,13 +152,9 @@
    1.12             error ("Unknown parameter: " ^ quote name ^ "."))
    1.13  
    1.14  
    1.15 -(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
    1.16 +(* Ensure that type systems such as "mono_simple?" and "poly_guards!!" are
    1.17     handled correctly. *)
    1.18 -fun implode_param [s, "?"] = s ^ "?"
    1.19 -  | implode_param [s, "??"] = s ^ "??"
    1.20 -  | implode_param [s, "!"] = s ^ "!"
    1.21 -  | implode_param [s, "!!"] = s ^ "!!"
    1.22 -  | implode_param ss = space_implode " " ss
    1.23 +val implode_param = strip_spaces_except_between_idents o space_implode " "
    1.24  
    1.25  structure Data = Theory_Data
    1.26  (