src/Tools/Code/code_preproc.ML

--- a/src/Tools/Code/code_preproc.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -213,7 +213,7 @@
     if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
     then (K I, ct)
     else
-     (K (Thm.instantiate (normalization, []) o Thm.varifyT_global),
+     (K (Thm.instantiate (TVars.make normalization, Vars.empty) o Thm.varifyT_global),
       Thm.cterm_of ctxt (map_types normalize t))
   end;