diff -r 1a85c1495d1f -r cc89a395b5a3 src/HOL/Algebra/Free_Abelian_Groups.thy
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Apr 05 15:02:46 2019 +0100
@@ -666,8 +666,7 @@
           have "finite {i \<in> I. Abs_poly_mapping (?f i) \<noteq> 0}"
             by (rule finite_subset [OF _ fin]) (use \<open>i \<in> I\<close> J_def eq in \<open>auto simp: in_keys_iff\<close>)
           with \<open>i \<in> I\<close> have "?h (\<lambda>j\<in>I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})"
-            apply (simp add: sum_diff1')
-            sorry
+            by (simp add: sum_diff1')
           then show ?thesis
             by (simp add: 1 2 Poly_Mapping.lookup_add)
         next