src/FOLP/simp.ML

 fun lhs_net_tac net =
   SUBGOAL(fn (prem,i) =>
           biresolve_tac (Net.unify_term net
                        (lhs_of (Logic.strip_assums_concl prem))) i);
 
-fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
+fun nth_subgoal i thm = nth (prems_of thm) (i - 1);
 
 fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
 
 fun lhs_of_eq i thm = lhs_of(goal_concl i thm)
 and rhs_of_eq i thm = rhs_of(goal_concl i thm);

     else case Seq.pull(cong_tac i thm) of
             SOME(thm',_) =>
                     let val ps = prems_of thm
                         and ps' = prems_of thm';
                         val n = length(ps')-length(ps);
-                        val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
+                        val a = length(Logic.strip_assums_hyp(nth ps (i - 1)))
                         val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
                     in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
           | NONE => (REW::ss,thm,anet,ats,cs);
 
 (*NB: the "Adding rewrites:" trace will look strange because assumptions