src/HOL/Nominal/Examples/W.thy

--- a/src/HOL/Nominal/Examples/W.thy	Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/Nominal/Examples/W.thy	Tue May 22 11:08: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> [x \<leftarrow> xs. x\<notin>set ys]"
+  "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs"
 
 lemma difference_eqvt_tvar[eqvt]:
   fixes pi::"tvar prm"