diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -305,8 +305,8 @@
     in
       Conv.fconv_rule Drule.beta_eta_conversion
          (case_thm
-            |> Thm.instantiate (type_cinsts, [])
-            |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
+            |> Thm.instantiate (TVars.make type_cinsts, Vars.empty)
+            |> Thm.instantiate (TVars.empty, Vars.make [(Pv, abs_ct), (Dv, free_ct)]))
     end;
 
 
@@ -1121,7 +1121,8 @@
   val gspec = Thm.forall_intr (Thm.cterm_of \<^context> x) spec
 in
 fun SPEC tm thm =
-   let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
+   let val gspec' =
+    Drule.instantiate_normalize (TVars.make [(TV, Thm.ctyp_of_cterm tm)], Vars.empty) gspec
    in thm RS (Thm.forall_elim tm gspec') end
 end;
 
@@ -1140,8 +1141,8 @@
       let val ctm2 = Thm.cterm_of ctxt tm2
       in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
   fun certify ctxt (ty_theta,tm_theta) =
-    (cty_theta ctxt (Vartab.dest ty_theta),
-     ctm_theta ctxt (Vartab.dest tm_theta))
+    (TVars.make (cty_theta ctxt (Vartab.dest ty_theta)),
+     Vars.make (ctm_theta ctxt (Vartab.dest tm_theta)))
 in
 fun GEN ctxt v th =
    let val gth = Thm.forall_intr v th