diff -r 5b8fccf0a48a -r 8f53fa93d5f0 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 20:20:59 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 20:45:55 2024 +0200
@@ -251,13 +251,17 @@
    complex we rely on instantiation to tell us if it applies
 *)
 fun equals_rsp_tac R ctxt =
-  case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *)  (* FIXME fragile *)
-    SOME ctm =>
+  case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *)
+    SOME ct =>
       let
-        val ty = domain_type (fastype_of R)
+        val T = Thm.ctyp_of_cterm ct
+        val A = Thm.dest_ctyp0 T
+        val try_inst =
+          \<^try>\<open>
+            Thm.instantiate (TVars.make1 ((("'a", 0), \<^sort>\<open>type\<close>), A),
+              Vars.make1 ((("R", 0), Thm.typ_of T), ct)) @{thm equals_rsp}\<close>
       in
-        case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
-            [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
+        case try_inst of
           SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
         | NONE => K no_tac
       end