more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 11 11:32:20 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 11 13:08:11 2024 +0200
@@ -255,11 +255,8 @@
     SOME ct =>
       let
         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>
+        val A = try Thm.dest_ctyp0 T
+        val try_inst = \<^try>\<open>Thm.instantiate' [SOME (the A)] [SOME ct] @{thm equals_rsp}\<close>
       in
         case try_inst of
           SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt