diff -r 5c579bb9adb1 -r 98cf1c823c48 src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Sun Jun 03 19:06:56 2018 +0200
+++ b/src/HOL/Nominal/Examples/W.thy	Wed Jun 06 11:12:37 2018 +0200
@@ -9,7 +9,7 @@
 abbreviation
   "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) 
 where
-  "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs"
+  "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
 
 lemma difference_eqvt_tvar[eqvt]:
   fixes pi::"tvar prm"