repaired snag in debug function
authorblanchet
Mon May 14 15:54:26 2012 +0200 (2012-05-14)
changeset 479191be466c58a26
parent 47918 81ae96996223
child 47920 a5c2386518e2
repaired snag in debug function
src/HOL/Tools/ATP/atp_proof_redirect.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Mon May 14 15:54:26 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Mon May 14 15:54:26 2012 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4    string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c
     1.5  
     1.6  val string_of_ref_graph =
     1.7 -  sequents_of_ref_graph #> map string_of_sequent #> implode
     1.8 +  sequents_of_ref_graph #> map string_of_sequent #> cat_lines
     1.9  
    1.10  fun redirect_sequent tainted bot (gamma, c) =
    1.11    if member atom_eq tainted c then