--- a/src/Pure/Proof/proof_checker.ML Tue Dec 05 20:07:52 2023 +0100
+++ b/src/Pure/Proof/proof_checker.ML Tue Dec 05 20:56:51 2023 +0100
@@ -78,9 +78,8 @@
fun thm_of_atom thm Ts =
let
val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
- val (fmap, thm') = Thm.varifyT_global' TFrees.empty thm;
- val ctye =
- (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
+ val (names, thm') = Thm.varifyT_global' TFrees.empty thm;
+ val ctye = tvars @ map #2 names ~~ map (Thm.global_ctyp_of thy) Ts;
in
Thm.instantiate (TVars.make ctye, Vars.empty)
(Thm.forall_intr_vars (Thm.forall_intr_frees thm'))