diff -r ca985e87c123 -r 037aaa0b6daf src/HOL/Proofs/Lambda/ListApplication.thy
--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Aug 03 07:31:25 2017 +0200
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Thu Aug 03 09:30:09 2017 +0200
@@ -127,7 +127,7 @@
   apply (rule trans_le_add1)
   apply (rule trans_le_add2)
   apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
-  apply (simp add: member_le_sum_list_nat)
+  apply (simp add: member_le_sum_list)
   done
 
 theorem Apps_dB_induct: