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 [];