--- 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 ())
--- 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
--- 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
--- 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
(