src/Provers/blast.ML

--- 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) =