more helpful error message
authorblanchet
Wed May 16 18:16:51 2012 +0200 (2012-05-16)
changeset 47930c06aa331bb76
parent 47929 3465c09222e0
child 47931 406d1df3787e
more helpful error message
src/HOL/Tools/ATP/atp_proof_redirect.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue May 15 12:07:16 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed May 16 18:16:51 2012 +0200
     1.3 @@ -153,7 +153,11 @@
     1.4  
     1.5  fun redirect_graph axioms tainted ref_graph =
     1.6    let
     1.7 -    val [bot] = Atom_Graph.maximals ref_graph
     1.8 +    val bot =
     1.9 +      case Atom_Graph.maximals ref_graph of
    1.10 +        [bot] => bot
    1.11 +      | bots => raise Fail ("malformed refutation graph with " ^
    1.12 +                            string_of_int (length bots) ^ " maximal nodes")
    1.13      val seqs =
    1.14        map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
    1.15      val direct_graph = direct_graph seqs