# HG changeset patch
# User blanchet
# Date 1315396217 -7200
# Node ID c9a081ef441d078d747c5d8b38290471be8519e6
# Parent  3634c6dba23f7bdfb80f6da9d8365431066f879e
tuning

diff -r 3634c6dba23f -r c9a081ef441d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -92,9 +92,6 @@
   InternalError |
   UnknownError of string
 
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
-
 fun elide_string threshold s =
   if size s > threshold then
     String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
@@ -475,7 +472,7 @@
 fun parse_line problem spass_names =
   parse_tstp_line problem || parse_spass_line spass_names
 fun parse_proof problem spass_names tstp =
-  tstp |> strip_spaces_except_between_ident_chars
+  tstp |> strip_spaces_except_between_idents
        |> raw_explode
        |> Scan.finite Symbol.stopper
               (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
diff -r 3634c6dba23f -r c9a081ef441d src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -10,6 +10,7 @@
   val hash_string : string -> int
   val hash_term : term -> int
   val strip_spaces : bool -> (char -> bool) -> string -> string
+  val strip_spaces_except_between_idents : string -> string
   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
@@ -88,6 +89,9 @@
 fun strip_spaces skip_comments is_evil =
   implode o strip_spaces_in_list skip_comments is_evil o String.explode
 
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_idents = strip_spaces true is_ident_char
+
 val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
diff -r 3634c6dba23f -r c9a081ef441d src/HOL/Tools/Nitpick/nitrox.ML
--- a/src/HOL/Tools/Nitpick/nitrox.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -21,8 +21,7 @@
 
 exception SYNTAX of string
 
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val tptp_explode = raw_explode o strip_spaces true is_ident_char
+val tptp_explode = raw_explode o strip_spaces_except_between_idents
 
 fun parse_file_path (c :: ss) =
     if c = "'" orelse c = "\"" then
diff -r 3634c6dba23f -r c9a081ef441d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -19,6 +19,7 @@
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
+open ATP_Util
 open ATP_Systems
 open ATP_Translate
 open Sledgehammer_Util
@@ -151,13 +152,9 @@
            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 "poly_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
+val implode_param = strip_spaces_except_between_idents o space_implode " "
 
 structure Data = Theory_Data
 (