diff -r b4564de51fa7 -r cc204e10385c src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Groups_List.thy	Wed Oct 23 16:09:23 2019 +0000
@@ -367,14 +367,18 @@
   "sum f (set [m..<n]) = sum_list (map f [m..<n])"
   by (simp add: interv_sum_list_conv_sum_set_nat)
 
-lemma sum_list_transfer[transfer_rule]:
+context
   includes lifting_syntax
-  assumes [transfer_rule]: "A 0 0"
-  assumes [transfer_rule]: "(A ===> A ===> A) (+) (+)"
-  shows "(list_all2 A ===> A) sum_list sum_list"
+begin
+
+lemma sum_list_transfer [transfer_rule]:
+  "(list_all2 A ===> A) sum_list sum_list"
+    if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)"
   unfolding sum_list.eq_foldr [abs_def]
   by transfer_prover
 
+end
+
 
 subsection \<open>List product\<close>