changeset 42364 | 8c674b3b8e44 |
parent 42012 | 2c3fe3cbebae |
child 42366 | 2305c70ec9b1 |
--- a/src/Provers/blast.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/blast.ML Sat Apr 16 18:11:20 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 (List.nth(prems_of st, i-1)) + val skoprem = fromSubgoal thy (nth (prems_of st) (i - 1)) val hyps = strip_imp_prems skoprem and concl = strip_imp_concl skoprem fun cont (tacs,_,choices) =