src/HOL/Tools/ATP/atp_proof.ML
changeset 40627 becf5d5187cc
parent 40553 1264c9172338
child 40669 5c316d1327d4
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4    fst o Scan.finite Symbol.stopper
     1.5              (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
     1.6                              (Scan.repeat1 parse_line)))
     1.7 -  o explode o strip_spaces_except_between_ident_chars
     1.8 +  o raw_explode o strip_spaces_except_between_ident_chars
     1.9  
    1.10  fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
    1.11  fun clean_up_dependencies _ [] = []