# HG changeset patch
# User wenzelm
# Date 1302978419 -7200
# Node ID 2305c70ec9b14d3a828f12f22999063b4a002800
# Parent  bfd28ba57859f5c192615685e3f496ae861686e7
more direct Thm.cprem_of (with exception THM instead of Subscript);

diff -r bfd28ba57859 -r 2305c70ec9b1 src/Provers/blast.ML
--- 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) =
diff -r bfd28ba57859 -r 2305c70ec9b1 src/Provers/hypsubst.ML
--- 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) =