--- a/src/Pure/Isar/code.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Isar/code.ML Sat Sep 04 22:17:15 2021 +0200
@@ -960,7 +960,7 @@
val _ = map (fn thm => if c = const_eqn thy thm then ()
else error ("Wrong head of code equation,\nexpected constant "
^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
- fun tvars_of T = rev (Term.add_tvarsT T []);
+ val tvars_of = build_rev o Term.add_tvarsT;
val vss = map (tvars_of o snd o head_eqn) thms;
fun inter_sorts vs =
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
--- a/src/Pure/Isar/subgoal.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML Sat Sep 04 22:17:15 2021 +0200
@@ -89,7 +89,7 @@
val prop = Thm.full_prop_of th';
val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
- val vars = rev (Term.add_vars prop []);
+ val vars = build_rev (Term.add_vars prop);
val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
fun var_inst v y =
--- a/src/Pure/Proof/extraction.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Proof/extraction.ML Sat Sep 04 22:17:15 2021 +0200
@@ -123,8 +123,8 @@
fun msg d s = writeln (Symbol.spaces d ^ s);
-fun vars_of t = map Var (rev (Term.add_vars t []));
-fun frees_of t = map Free (rev (Term.add_frees t []));
+fun vars_of t = map Var (build_rev (Term.add_vars t));
+fun frees_of t = map Free (build_rev (Term.add_frees t));
fun vfs_of t = vars_of t @ frees_of t;
val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
@@ -385,7 +385,7 @@
val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
SOME (TVar (("'" ^ v, i), [])) else NONE)
- (rev (Term.add_vars prop' []));
+ (build_rev (Term.add_vars prop'));
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
fun typ_map T = Type.strip_sorts
--- a/src/Pure/Proof/proof_checker.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML Sat Sep 04 22:17:15 2021 +0200
@@ -76,7 +76,7 @@
fun thm_of_atom thm Ts =
let
- val tvars = rev (Term.add_tvars (Thm.full_prop_of thm) []);
+ val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm;
val ctye =
(tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
--- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat Sep 04 22:17:15 2021 +0200
@@ -249,7 +249,7 @@
if member (op =) defs s then
let
val vs = vars_of prop;
- val tvars = rev (Term.add_tvars prop []);
+ val tvars = build_rev (Term.add_tvars prop);
val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
--- 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;
--- a/src/Pure/Tools/rule_insts.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML Sat Sep 04 22:17:15 2021 +0200
@@ -174,8 +174,8 @@
| zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest
| zip_vars [] _ = error "More instantiations than variables in theorem";
val insts =
- zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
- zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
+ zip_vars (build_rev (Term.add_vars (Thm.full_prop_of thm))) args @
+ zip_vars (build_rev (Term.add_vars (Thm.concl_of thm))) concl_args;
in where_rule ctxt insts fixes thm end;
fun read_instantiate ctxt insts xs =
--- 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]);
--- 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))))
--- a/src/Pure/proofterm.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/proofterm.ML Sat Sep 04 22:17:15 2021 +0200
@@ -1125,7 +1125,7 @@
| is_fun (TVar _) = true
| is_fun _ = false;
-fun vars_of t = map Var (rev (Term.add_vars t []));
+fun vars_of t = map Var (build_rev (Term.add_vars t));
fun add_funvars Ts (vs, t) =
if is_fun (fastype_of1 (Ts, t)) then
--- a/src/Pure/thm.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/thm.ML Sat Sep 04 22:17:15 2021 +0200
@@ -1752,7 +1752,7 @@
fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
val _ = null hyps orelse err "bad hyps";
val _ = null tpairs orelse err "bad flex-flex constraints";
- val tfrees = rev (Term.add_tfree_names prop []);
+ val tfrees = build_rev (Term.add_tfree_names prop);
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
val ps = map (apsnd (Future.map fulfill_body)) promises;
@@ -2257,7 +2257,7 @@
fun standard_tvars thm =
let
val thy = theory_of_thm thm;
- val tvars = rev (Term.add_tvars (prop_of thm) []);
+ val tvars = build_rev (Term.add_tvars (prop_of thm));
val names = Name.invent Name.context Name.aT (length tvars);
val tinst =
map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
--- a/src/Pure/variable.ML Sat Sep 04 22:05:35 2021 +0200
+++ b/src/Pure/variable.ML Sat Sep 04 22:17:15 2021 +0200
@@ -591,7 +591,7 @@
fun importT_inst ts ctxt =
let
- val tvars = rev (fold Term.add_tvars ts []);
+ val tvars = build_rev (fold Term.add_tvars ts);
val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
val instT =
Term_Subst.TVars.build (fold2 (fn a => fn b =>
@@ -602,7 +602,7 @@
let
val ren = Name.clean #> (if is_open then I else Name.internal);
val (instT, ctxt') = importT_inst ts ctxt;
- val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
+ val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
val inst =
Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>