# HG changeset patch # User blanchet # Date 1337003666 -7200 # Node ID 1be466c58a264f90944848143badd6696045dcab # Parent 81ae9699622302426045c59200e6424ac644ef06 repaired snag in debug function 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