changeset 47919 | 1be466c58a26 |
parent 47915 | 5b1a737777c9 |
child 47928 | fb2bc5a1eb32 |
--- 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 ^ " \<turnstile> " ^ 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