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