src/HOL/Tools/Quotient/quotient_tacs.ML

 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
 
 fun quotient_tac ctxt =
   (REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm identity_quotient},
+    [rtac @{thm identity_quotient3},
      resolve_tac (Quotient_Info.quotient_rules ctxt)]))
 
 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
 

               val ty_f = range_type (fastype_of f)
               val thy = Proof_Context.theory_of context
               val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
               val inst_thm = Drule.instantiate' ty_inst
-                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
             in
               (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
             end
       | _ => no_tac
     end)

     val thy =  Proof_Context.theory_of lthy
     val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy)
     val prs = Quotient_Info.prs_rules lthy
     val ids = Quotient_Info.id_simps lthy
     val thms =
-      @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
+      @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
 
     val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [
       map_fun_tac lthy,