--- 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