1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 07 13:50:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -92,9 +92,6 @@
     1.4    InternalError |
     1.5    UnknownError of string
     1.6  
     1.7 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
     1.8 -val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
     1.9 -
    1.10  fun elide_string threshold s =
    1.11    if size s > threshold then
    1.12      String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
    1.13 @@ -475,7 +472,7 @@
    1.14  fun parse_line problem spass_names =
    1.15    parse_tstp_line problem || parse_spass_line spass_names
    1.16  fun parse_proof problem spass_names tstp =
    1.17 -  tstp |> strip_spaces_except_between_ident_chars
    1.18 +  tstp |> strip_spaces_except_between_idents
    1.19         |> raw_explode
    1.20         |> Scan.finite Symbol.stopper
    1.21                (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Wed Sep 07 13:50:17 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Sep 07 13:50:17 2011 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4    val hash_string : string -> int
     2.5    val hash_term : term -> int
     2.6    val strip_spaces : bool -> (char -> bool) -> string -> string
     2.7 +  val strip_spaces_except_between_idents : string -> string
     2.8    val nat_subscript : int -> string
     2.9    val unyxml : string -> string
    2.10    val maybe_quote : string -> string
    2.11 @@ -88,6 +89,9 @@
    2.12  fun strip_spaces skip_comments is_evil =
    2.13    implode o strip_spaces_in_list skip_comments is_evil o String.explode
    2.14  
    2.15 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    2.16 +val strip_spaces_except_between_idents = strip_spaces true is_ident_char
    2.17 +
    2.18  val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
    2.19  fun nat_subscript n =
    2.20    n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript

     3.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML	Wed Sep 07 13:50:17 2011 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitrox.ML	Wed Sep 07 13:50:17 2011 +0200
     3.3 @@ -21,8 +21,7 @@
     3.4  
     3.5  exception SYNTAX of string
     3.6  
     3.7 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
     3.8 -val tptp_explode = raw_explode o strip_spaces true is_ident_char
     3.9 +val tptp_explode = raw_explode o strip_spaces_except_between_idents
    3.10  
    3.11  fun parse_file_path (c :: ss) =
    3.12      if c = "'" orelse c = "\"" then

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
     4.3 @@ -19,6 +19,7 @@
     4.4  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
     4.5  struct
     4.6  
     4.7 +open ATP_Util
     4.8  open ATP_Systems
     4.9  open ATP_Translate
    4.10  open Sledgehammer_Util
    4.11 @@ -151,13 +152,9 @@
    4.12             error ("Unknown parameter: " ^ quote name ^ "."))
    4.13  
    4.14  
    4.15 -(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
    4.16 +(* Ensure that type systems such as "mono_simple?" and "poly_guards!!" are
    4.17     handled correctly. *)
    4.18 -fun implode_param [s, "?"] = s ^ "?"
    4.19 -  | implode_param [s, "??"] = s ^ "??"
    4.20 -  | implode_param [s, "!"] = s ^ "!"
    4.21 -  | implode_param [s, "!!"] = s ^ "!!"
    4.22 -  | implode_param ss = space_implode " " ss
    4.23 +val implode_param = strip_spaces_except_between_idents o space_implode " "
    4.24  
    4.25  structure Data = Theory_Data
    4.26  (