src/Pure/drule.ML

           AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu)));
       in infer_instantiate_types ctxt args' th end;
 
 fun infer_instantiate' ctxt args th =
   let
-    val vars = rev (Term.add_vars (Thm.full_prop_of th) []);
+    val vars = build_rev (Term.add_vars (Thm.full_prop_of th));
     val args' = zip_options vars args
       handle ListPair.UnequalLengths =>
         raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]);
   in infer_instantiate_types ctxt args' th end;