src/HOL/Number_Theory/Residues.thy

--- a/src/HOL/Number_Theory/Residues.thy	Sat Jun 16 22:09:24 2018 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Sun Jun 17 22:00:43 2018 +0100
@@ -348,7 +348,7 @@
     done
   also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
     apply (subst finprod_Union_disjoint)
-       apply auto
+       apply (auto simp: pairwise_def disjnt_def)
      apply (metis Units_inv_inv)+
     done
   also have "\<dots> = \<one>"