src/Provers/eqsubst.ML

--- a/src/Provers/eqsubst.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Provers/eqsubst.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -363,7 +363,7 @@
       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
       val cfvs = rev (map ctermify fvs);
 
-      val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
+      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
       val asm_nprems = length (Logic.strip_imp_prems asmt);
 
       val pth = trivify asmt;