src/Pure/term.ML

         val (u', Ts'') = replace_types u Ts';
       in (t' $ u', Ts'') end;
 
 fun burrow_types f ts =
   let
-    val Ts = rev (fold (fold_types cons) ts []);
+    val Ts = rev ((fold o fold_types) cons ts []);
     val Ts' = f Ts;
     val (ts', []) = fold_map replace_types ts Ts';
   in ts' end;
 
 (*collect variables*)