src/HOL/Tools/code_evaluation.ML

 fun mk_term_of_eq thy ty (c, (_, tys)) =
   let
     val t = list_comb (Const (c, tys ---> ty),
       map Free (Name.invent_names Name.context "a" tys));
     val (arg, rhs) =
-      pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
-        (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+      pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
+        (t,
+          map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
+            (HOLogic.reflect_term t));
     val cty = Thm.ctyp_of thy ty;
   in
     @{thm term_of_anything}
     |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
     |> Thm.varifyT_global