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