--- a/src/HOL/Old_Number_Theory/Euler.thy Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Sat Jun 28 09:16:42 2014 +0200
@@ -180,7 +180,7 @@
proof -
from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
by (auto simp add: SetS_finite SetS_elems_finite
- MultInvPair_prop1c setprod_Union_disjoint)
+ MultInvPair_prop1c setprod.Union_disjoint)
also have "[setprod (setprod (%x. x)) (SetS a p) =
setprod (%x. a) (SetS a p)] (mod p)"
by (rule setprod_same_function_zcong)