diff -r 3fba6741ead2 -r 914436eb988b src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 15:43:51 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 16:21:04 2013 +0100
@@ -165,7 +165,10 @@
           val provable =
             filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
           val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
-          val seq as (gamma, c) = hd (horn_provable @ provable)
+          val seq as (gamma, c) =
+            case horn_provable @ provable of
+              [] => raise Fail "ill-formed refutation graph"
+            | next :: _ => next
         in
           Have (map single gamma, c) ::
           redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)