1.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 15:43:51 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 16:21:04 2013 +0100
     1.3 @@ -165,7 +165,10 @@
     1.4            val provable =
     1.5              filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
     1.6            val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
     1.7 -          val seq as (gamma, c) = hd (horn_provable @ provable)
     1.8 +          val seq as (gamma, c) =
     1.9 +            case horn_provable @ provable of
    1.10 +              [] => raise Fail "ill-formed refutation graph"
    1.11 +            | next :: _ => next
    1.12          in
    1.13            Have (map single gamma, c) ::
    1.14            redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)