diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/List.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -3836,7 +3836,7 @@
 text{* Courtesy of Matthias Daum: *}
 lemma append_replicate_commute:
   "replicate n x @ replicate k x = replicate k x @ replicate n x"
-apply (simp add: replicate_add [THEN sym])
+apply (simp add: replicate_add [symmetric])
 apply (simp add: add.commute)
 done