src/Provers/hypsubst.ML
changeset 42366 2305c70ec9b1
parent 42364 8c674b3b8e44
child 42799 4e33894aec6d
--- a/src/Provers/hypsubst.ML	Sat Apr 16 20:22:50 2011 +0200
+++ b/src/Provers/hypsubst.ML	Sat Apr 16 20:26:59 2011 +0200
@@ -219,7 +219,7 @@
       | imptac (r, hyp::hyps) st =
           let
             val (hyp', _) =
-              nth (prems_of st) (i - 1)
+              term_of (Thm.cprem_of st i)
               |> Logic.strip_assums_concl
               |> Data.dest_Trueprop |> Data.dest_imp;
             val (r', tac) =