# HG changeset patch # User wenzelm # Date 1630786635 -7200 # Node ID dbaed92fd8afcf9c6678f462822330ece7c60518 # Parent 4f2bd13edce3be77987e434afe130f5224f6a784 tuned signature; diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Isar/code.ML --- 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 []; diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Isar/subgoal.ML --- 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 = diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Proof/extraction.ML --- 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 diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Proof/proof_checker.ML --- 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); diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Proof/proof_rewrite_rules.ML --- 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), diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Thy/export_theory.ML --- 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; diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/Tools/rule_insts.ML --- 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 = diff -r 4f2bd13edce3 -r dbaed92fd8af 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]); 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)))) diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/proofterm.ML --- 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 diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/thm.ML --- 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; diff -r 4f2bd13edce3 -r dbaed92fd8af src/Pure/variable.ML --- 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 =>