src/Provers/blast.ML
changeset 42366 2305c70ec9b1
parent 42364 8c674b3b8e44
child 42369 167e8ba0f4b1
--- a/src/Provers/blast.ML	Sat Apr 16 20:22:50 2011 +0200
+++ b/src/Provers/blast.ML	Sat Apr 16 20:26:59 2011 +0200
@@ -1252,7 +1252,7 @@
   let val thy = Thm.theory_of_thm st0
       val state = initialize thy
       val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
-      val skoprem = fromSubgoal thy (nth (prems_of st) (i - 1))
+      val skoprem = fromSubgoal thy (Thm.term_of (Thm.cprem_of st i))
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem
       fun cont (tacs,_,choices) =