--- a/src/HOL/Computational_Algebra/Primes.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy Thu Feb 15 12:11:00 2018 +0100
@@ -728,7 +728,7 @@
define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
define A where "A = Abs_multiset g"
have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
- from finite_subset[OF this assms(1)] have [simp]: "g : multiset"
+ from finite_subset[OF this assms(1)] have [simp]: "g \<in> multiset"
by (simp add: multiset_def)
from assms have count_A: "count A x = g x" for x unfolding A_def
by simp