# HG changeset patch
# User blanchet
# Date 1360257871 -3600
# Node ID b0d9ff6b4b4f479c6dfef0e40532b4099f4099c6
# Parent  211a9240b1e3faab4188b430e6166b44e78393f1
more precise error message

diff -r 211a9240b1e3 -r b0d9ff6b4b4f src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Thu Feb 07 14:05:33 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Thu Feb 07 18:24:31 2013 +0100
@@ -152,8 +152,10 @@
     val bot =
       case Atom_Graph.maximals ref_graph of
         [bot] => bot
-      | bots => raise Fail ("malformed refutation graph with " ^
-                            string_of_int (length bots) ^ " maximal nodes")
+      | bots =>
+        raise Fail ("Malformed refutation graph with " ^
+                    string_of_int (length bots) ^ " maximal nodes (" ^
+                    commas_quote (map Atom.string_of bots) ^ ")")
     val seqs =
       map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
     val direct_graph = direct_graph seqs