--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -12,7 +12,7 @@
 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
 fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
   let
-    val cgoal = nth (cprems_of st) (i - 1);
+    val cgoal = nth (Thm.cprems_of st) (i - 1);
     val maxidx = Thm.maxidx_of_cterm cgoal;
     val j = maxidx + 1;
     val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst;