# HG changeset patch
# User blanchet
# Date 1284639888 -7200
# Node ID b505208f435d565ca9d5d4b83aa0442b464f596d
# Parent  37f1a961a91817ada3752ea2a7a699949ed0986e
avoid code duplication

diff -r 37f1a961a918 -r b505208f435d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 14:24:03 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 14:24:48 2010 +0200
@@ -19,6 +19,7 @@
 
   type 'a proof = 'a uniform_formula step list
 
+  val strip_spaces : (char -> bool) -> string -> string
   val is_same_step : step_name * step_name -> bool
   val atp_proof_from_tstplike_string : string -> string proof
   val map_term_names_in_atp_proof :
@@ -29,7 +30,6 @@
 structure ATP_Proof : ATP_PROOF =
 struct
 
-(*### FIXME: DUPLICATED FROM SLEDGEHAMMER_UTIL *)
 fun strip_spaces_in_list _ [] = []
   | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
   | strip_spaces_in_list is_evil [c1, c2] =
@@ -221,7 +221,7 @@
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
                             (Scan.repeat1 parse_line)))
-  o explode o strip_spaces_except_between_ident_chars (*### FIXME: why isn't strip_spaces enough?*)
+  o explode o strip_spaces_except_between_ident_chars
 
 fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
 fun clean_up_dependencies _ [] = []
diff -r 37f1a961a918 -r b505208f435d src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 16 14:24:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 16 14:24:48 2010 +0200
@@ -10,7 +10,6 @@
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
-  val strip_spaces_except_between_ident_chars : string -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
   val scan_integer : string list -> int * string list
@@ -41,28 +40,7 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
 
-fun strip_spaces_in_list _ [] = []
-  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
-  | strip_spaces_in_list is_evil [c1, c2] =
-    strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2]
-  | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
-    if Char.isSpace c1 then
-      strip_spaces_in_list is_evil (c2 :: c3 :: cs)
-    else if Char.isSpace c2 then
-      if Char.isSpace c3 then
-        strip_spaces_in_list is_evil (c1 :: c3 :: cs)
-      else
-        str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
-        strip_spaces_in_list is_evil (c3 :: cs)
-    else
-      str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs)
-fun strip_spaces is_evil =
-  implode o strip_spaces_in_list is_evil o String.explode
-
-val simplify_spaces = strip_spaces (K true)
-
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
+val simplify_spaces = ATP_Proof.strip_spaces (K true)
 
 fun parse_bool_option option name s =
   (case s of