--- a/src/Pure/Thy/export_theory.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Thy/export_theory.ML Sat Sep 04 22:17:15 2021 +0200
@@ -78,7 +78,7 @@
SOME goal => Thm.prems_of goal
| NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
end;
- val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
+ val typargs = build_rev (fold Term.add_tfrees (map (Free o #1) args @ axioms));
in {typargs = typargs, args = args, axioms = axioms} end;
fun get_locales thy =
@@ -148,8 +148,8 @@
{props = pos_properties pos,
name = name,
rough_classification = rough_classification,
- typargs = rev (fold Term.add_tfrees spec []),
- args = rev (fold Term.add_frees spec []),
+ typargs = build_rev (fold Term.add_tfrees spec),
+ args = build_rev (fold Term.add_frees spec),
terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
rules = drop (length terms) spec}
end;