1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 14:24:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 14:24:48 2010 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  
     1.5    type 'a proof = 'a uniform_formula step list
     1.6  
     1.7 +  val strip_spaces : (char -> bool) -> string -> string
     1.8    val is_same_step : step_name * step_name -> bool
     1.9    val atp_proof_from_tstplike_string : string -> string proof
    1.10    val map_term_names_in_atp_proof :
    1.11 @@ -29,7 +30,6 @@
    1.12  structure ATP_Proof : ATP_PROOF =
    1.13  struct
    1.14  
    1.15 -(*### FIXME: DUPLICATED FROM SLEDGEHAMMER_UTIL *)
    1.16  fun strip_spaces_in_list _ [] = []
    1.17    | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
    1.18    | strip_spaces_in_list is_evil [c1, c2] =
    1.19 @@ -221,7 +221,7 @@
    1.20    fst o Scan.finite Symbol.stopper
    1.21              (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
    1.22                              (Scan.repeat1 parse_line)))
    1.23 -  o explode o strip_spaces_except_between_ident_chars (*### FIXME: why isn't strip_spaces enough?*)
    1.24 +  o explode o strip_spaces_except_between_ident_chars
    1.25  
    1.26  fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
    1.27  fun clean_up_dependencies _ [] = []

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 16 14:24:03 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 16 14:24:48 2010 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4    val plural_s : int -> string
     2.5    val serial_commas : string -> string list -> string list
     2.6    val simplify_spaces : string -> string
     2.7 -  val strip_spaces_except_between_ident_chars : string -> string
     2.8    val parse_bool_option : bool -> string -> string -> bool option
     2.9    val parse_time_option : string -> string -> Time.time option
    2.10    val scan_integer : string list -> int * string list
    2.11 @@ -41,28 +40,7 @@
    2.12    | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    2.13    | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    2.14  
    2.15 -fun strip_spaces_in_list _ [] = []
    2.16 -  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
    2.17 -  | strip_spaces_in_list is_evil [c1, c2] =
    2.18 -    strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2]
    2.19 -  | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
    2.20 -    if Char.isSpace c1 then
    2.21 -      strip_spaces_in_list is_evil (c2 :: c3 :: cs)
    2.22 -    else if Char.isSpace c2 then
    2.23 -      if Char.isSpace c3 then
    2.24 -        strip_spaces_in_list is_evil (c1 :: c3 :: cs)
    2.25 -      else
    2.26 -        str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
    2.27 -        strip_spaces_in_list is_evil (c3 :: cs)
    2.28 -    else
    2.29 -      str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs)
    2.30 -fun strip_spaces is_evil =
    2.31 -  implode o strip_spaces_in_list is_evil o String.explode
    2.32 -
    2.33 -val simplify_spaces = strip_spaces (K true)
    2.34 -
    2.35 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    2.36 -val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
    2.37 +val simplify_spaces = ATP_Proof.strip_spaces (K true)
    2.38  
    2.39  fun parse_bool_option option name s =
    2.40    (case s of