1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 16:13:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 16:54:12 2010 +0200
     1.3 @@ -417,7 +417,9 @@
     1.4                 AAnd => s_conj
     1.5               | AOr => s_disj
     1.6               | AImplies => s_imp
     1.7 -             | AIff => s_iff)
     1.8 +             | AIf => s_imp o swap
     1.9 +             | AIff => s_iff
    1.10 +             | ANotIff => s_not o s_iff)
    1.11        | AAtom tm => term_from_pred thy full_types tfrees pos tm
    1.12        | _ => raise FORMULA [phi]
    1.13    in repair_tvar_sorts (do_formula true phi Vartab.empty) end
    1.14 @@ -719,7 +721,10 @@
    1.15         conjecture. The second pass flips the proof by contradiction to obtain a
    1.16         direct proof, introducing case splits when an inference depends on
    1.17         several facts that depend on the negated conjecture. *)
    1.18 -    fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
    1.19 +    fun find_hyp num =
    1.20 +      nth hyp_ts (index_in_shape num conjecture_shape)
    1.21 +      handle Subscript =>
    1.22 +             raise Fail ("Cannot find hypothesis " ^ Int.toString num)
    1.23      val concl_l = (raw_prefix, List.last conjecture_shape)
    1.24      fun first_pass ([], contra) = ([], contra)
    1.25        | first_pass ((step as Fix _) :: proof, contra) =