src/HOL/Computational_Algebra/Factorial_Ring.thy
 changeset 66938 c78ff0aeba4c parent 66453 cc19f7ca2ed6 child 67051 e7e54a0b9197
```     1.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 30 13:18:44 2017 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 30 13:18:44 2017 +0000
1.3 @@ -1424,7 +1424,7 @@
1.4    define A where "A = Abs_multiset f"
1.5    from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
1.6    with S(2) have nz: "n \<noteq> 0" by auto
1.7 -  from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
1.8 +  from S_eq \<open>finite S\<close> have count_A: "count A = f"
1.9      unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
1.10    from S_eq count_A have set_mset_A: "set_mset A = S"
1.11      by (simp only: set_mset_def)
1.12 @@ -1452,7 +1452,8 @@
1.13      also from S(1) p
1.14      have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
1.15        by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
1.16 -    also have "sum_mset \<dots> = f p" by (simp add: sum_mset_delta' count_A)
1.17 +    also have "sum_mset \<dots> = f p"
1.18 +      by (simp add: semiring_1_class.sum_mset_delta' count_A)
1.19      finally show "f p = multiplicity p n" ..
1.20    qed
1.21  qed
```