src/HOL/Tools/Quotient/quotient_tacs.ML

     (* merge with previous tactic *)
     Cong_Tac.cong_tac ctxt @{thm cong} THEN'
                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
 
     (* resolving with R x y assumptions *)
-    atac,
+    assume_tac ctxt,
 
     (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
     rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
 
     (* reflexivity of the basic relations *)

       val vrs = Term.add_frees concl []
       val cvrs = map (cterm_of thy o Free) vrs
       val concl' = apply_under_Trueprop (all_list vrs) concl
       val goal = Logic.mk_implies (concl', concl)
       val rule = Goal.prove ctxt [] [] goal
-        (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+        (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
     in
       rtac rule i
     end)