diff -r 81ae96996223 -r 1be466c58a26 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Mon May 14 15:54:26 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Mon May 14 15:54:26 2012 +0200 @@ -97,7 +97,7 @@ string_of_context gamma ^ " \ " ^ Atom.string_of c val string_of_ref_graph = - sequents_of_ref_graph #> map string_of_sequent #> implode + sequents_of_ref_graph #> map string_of_sequent #> cat_lines fun redirect_sequent tainted bot (gamma, c) = if member atom_eq tainted c then