diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Analysis/normarith.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -359,7 +359,7 @@
   val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
   val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
   val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
-  val cps = map (swap o Thm.dest_equals) (cprems_of th11)
+  val cps = map (swap o Thm.dest_equals) (Thm.cprems_of th11)
   val th12 = Drule.instantiate_normalize (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cps)) th11
   val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
  in hd (Variable.export ctxt' ctxt [th13])