--- a/src/Pure/Isar/class.ML	2026-10-11 23:26:48.897196169 +0200
+++ b/src/Pure/Isar/class.ML	2026-10-11 23:27:03.905239331 +0200
@@ -281,14 +281,24 @@
       |> map (fn (v, T) => Var ((v, 0), T));
   in (betapplys (t, vts), betapplys (Const c_ty, vts)) end;
 
-fun these_unchecks thy =
-  these_operations thy
-  #> map_filter (fn (c, (_, ((ty, t), input_only))) =>
+(*operations are registered at the base sort of their own class; in the context of a class
+  whose base sort is finer, the class parameters live at that finer sort, so the operations
+  must be retyped to the base sort of the context they are used in*)
+fun these_operations_at thy sort base_sort =
+  let val retypeT = map_type_tfree (K (Term.aT base_sort))
+  in
+    these_operations thy sort
+    |> (map o apsnd o apsnd o apfst) (fn (ty, t) => (retypeT ty, Term.map_types retypeT t))
+  end;
+
+fun these_unchecks thy sort base_sort =
+  these_operations_at thy sort base_sort
+  |> map_filter (fn (c, (_, ((ty, t), input_only))) =>
     if input_only then NONE else SOME (make_rewrite t (c, ty)));
 
-fun these_unchecks_reversed thy =
-  these_operations thy
-  #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t));
+fun these_unchecks_reversed thy sort base_sort =
+  these_operations_at thy sort base_sort
+  |> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t));
 
 fun redeclare_const thy c =
   let val b = Long_Name.base_name c
@@ -298,7 +308,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
-    val operations = these_operations thy sort;
+    val operations = these_operations_at thy sort base_sort;
     fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
     val primary_constraints =
       (map o apsnd) (subst_class_typ base_sort o fst o fst o snd) operations;
@@ -318,7 +328,7 @@
           | NONE => NONE)
       | NONE => NONE);
     fun subst (c, _) = Option.map (fst o snd) (AList.lookup (op =) operations c);
-    val unchecks = these_unchecks thy sort;
+    val unchecks = these_unchecks thy sort base_sort;
   in
     ctxt
     |> fold (redeclare_const thy o fst) primary_constraints
@@ -449,7 +459,8 @@
 fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val preprocess = perhaps (try (Pattern.rewrite_term_yoyo thy (these_unchecks thy [class]) []));
+    val preprocess = perhaps (try (Pattern.rewrite_term_yoyo thy
+      (these_unchecks thy [class] (base_sort thy class)) []));
     val (global_rhs, (_, (_, term_params))) =
       Generic_Target.export_abbrev lthy preprocess rhs;
     val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
@@ -471,7 +482,8 @@
     val thy = Proof_Context.theory_of lthy;
     val phi = morphism lthy class;
     val rhs_generic =
-      perhaps (try (Pattern.rewrite_term_yoyo thy (these_unchecks_reversed thy [class]) [])) rhs;
+      perhaps (try (Pattern.rewrite_term_yoyo thy
+        (these_unchecks_reversed thy [class] (base_sort thy class)) [])) rhs;
   in
     lthy
     |> canonical_abbrev_target class phi prmode ((b, mx), rhs)