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