--- 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))))