src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML

 fun parse_lines pool = Scan.repeat1 (parse_line pool)
 fun parse_proof pool =
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
                             (parse_lines pool)))
-  o explode o strip_spaces
+  o explode o strip_spaces_except_between_ident_chars
 
 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
 
 exception FO_TERM of string fo_term list
 exception FORMULA of (string, string fo_term) formula list