--- a/Nominal/FSet.thy	Thu Apr 22 12:33:51 2010 +0200
+++ b/Nominal/FSet.thy	Thu Apr 22 12:42:15 2010 +0200
@@ -1070,7 +1070,8 @@
   "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
   by (lifting sub_list_cons)
 
-thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars]
+lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+  by (lifting sub_list_def[simplified memb_def[symmetric]])
 
 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
 by (rule meta_eq_to_obj_eq)