src/HOL/Old_Number_Theory/Chinese.thy

         apply (tactic {* stac (@{thm zcong_zmod} RS sym) 6 *})
         apply (subgoal_tac [6]
           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
          prefer 6
-         apply (simp add: mult_ac)
+         apply (simp add: ac_simps)
         apply (unfold xilin_sol_def)
         apply (tactic {* asm_simp_tac @{context} 6 *})
         apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
         apply (rule_tac [6] unique_xi_sol)
            apply (rule_tac [3] funprod_zdvd)