src/HOL/Old_Number_Theory/Factorization.thy

   apply blast
   done
 
 lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
   apply (induct set: perm)
-     apply (simp_all add: mult_ac)
+     apply (simp_all add: ac_simps)
   done
 
 lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
   apply (induct set: perm)
      apply auto