# HG changeset patch
# User blanchet
# Date 1337185011 -7200
# Node ID c06aa331bb76232c57672ef415780e31746ba1b3
# Parent  3465c09222e0099f3c635bc91136b7ab0c1e77ee
more helpful error message

diff -r 3465c09222e0 -r c06aa331bb76 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue May 15 12:07:16 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed May 16 18:16:51 2012 +0200
@@ -153,7 +153,11 @@
 
 fun redirect_graph axioms tainted ref_graph =
   let
-    val [bot] = Atom_Graph.maximals ref_graph
+    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")
     val seqs =
       map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
     val direct_graph = direct_graph seqs