src/HOL/Tools/Quotient/quotient_tacs.ML

 
 fun equiv_tac ctxt =
   REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
 
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
-val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
 
 fun quotient_tac ctxt =
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
 
 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver =
-  Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
 
 fun solve_quotient_assm ctxt thm =
   case Seq.pull (quotient_tac ctxt 1 thm) of
     SOME (t, _) => t
   | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."