diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/coinduction.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -69,8 +69,8 @@
               |> fold Variable.declare_thm (raw_thm :: prems);
             val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
             val (instT, inst) = Thm.match (thm_concl, concl);
-            val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
-            val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
+            val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) (TVars.dest instT);
+            val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) (Vars.dest inst);
             val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
               |> map (subst_atomic_types rhoTs);
             val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;