# HG changeset patch
# User blanchet
# Date 1337003666 -7200
# Node ID 5b1a737777c98ac4b2f9b3f75996e7846c8ffda9
# Parent  94f37848b7c9117af1d4ee22b5629e3ffed63fd1
added debugging function

diff -r 94f37848b7c9 -r 5b1a737777c9 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Mon May 14 15:54:26 2012 +0200
@@ -37,6 +37,7 @@
   val axioms_of_ref_graph : ref_graph -> atom list -> atom list
   val tainted_atoms_of_ref_graph : ref_graph -> atom list -> atom list
   val sequents_of_ref_graph : ref_graph -> ref_sequent list
+  val string_of_ref_graph : ref_graph -> string
   val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
   val direct_graph : direct_sequent list -> direct_graph
   val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
@@ -90,6 +91,14 @@
   map (`(Atom_Graph.immediate_preds ref_graph))
       (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))
 
+val string_of_context = map Atom.string_of #> space_implode ", "
+
+fun string_of_sequent (gamma, c) =
+  string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c
+
+val string_of_ref_graph =
+  sequents_of_ref_graph #> map string_of_sequent #> implode
+
 fun redirect_sequent tainted bot (gamma, c) =
   if member atom_eq tainted c then
     gamma |> List.partition (not o member atom_eq tainted)