src/Pure/drule.ML

--- a/src/Pure/drule.ML	Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/drule.ML	Sat Sep 04 22:17:15 2021 +0200
@@ -795,7 +795,7 @@
 
 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]);