diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/more_thm.ML	Sat Sep 04 22:17:15 2021 +0200
@@ -438,9 +438,9 @@
         err "more instantiations than variables in thm";
 
     val thm' =
-      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
+      Thm.instantiate ((zip_vars (build_rev (Thm.fold_terms Term.add_tvars thm)) cTs), []) thm;
     val thm'' =
-      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
+      Thm.instantiate ([], zip_vars (build_rev (Thm.fold_terms Term.add_vars thm')) cts) thm';
   in thm'' end;
 
 
@@ -532,7 +532,7 @@
 
 fun stripped_sorts thy t =
   let
-    val tfrees = rev (Term.add_tfrees t []);
+    val tfrees = build_rev (Term.add_tfrees t);
     val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees));
     val recover =
       map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))