src/Pure/pattern.ML

 val trace_unify_fail = ref false;
 
 fun string_of_term thy env binders t = Sign.string_of_term thy
   (Envir.norm_term env (subst_bounds(map Free binders,t)));
 
-fun bname binders i = fst(List.nth(binders,i));
+fun bname binders i = fst (nth binders i);
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
 fun typ_clash thy (tye,T,U) =
   if !trace_unify_fail
   then let val t = Sign.string_of_typ thy (Envir.norm_type tye T)

     in mpb 0 end;
 
 fun idx [] j     = raise Unif
   | idx(i::is) j = if (i:int) =j then length is else idx is j;
 
-fun at xs i = List.nth (xs,i);
-
 fun mkabs (binders,is,t)  =
-    let fun mk(i::is) = let val (x,T) = List.nth(binders,i)
+    let fun mk(i::is) = let val (x,T) = nth binders i
                         in Abs(x,T,mk is) end
           | mk []     = t
     in mk is end;
 
 val incr = mapbnd (fn i => i+1);

 fun app (s,(i::is)) = app (s$Bound(i),is)
   | app (s,[])      = s;
 
 fun red (Abs(_,_,s)) (i::is) js = red s is (i::js)
   | red t            []      [] = t
-  | red t            is      jn = app (mapbnd (at jn) t,is);
+  | red t            is      jn = app (mapbnd (nth jn) t,is);
 
 
 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *)
 fun split_type (T,0,Ts)                    = (Ts,T)
   | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
   | split_type _                           = error("split_type");
 
 fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
   let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
-  in map (at Ts) is ---> U end;
+  in map (nth Ts) is ---> U end;
 
 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
 
 fun mknewhnf(env,binders,is,F as (a,_),T,js) =
   let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))