diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -32,10 +32,6 @@
   by blast
 
 lemma [code func]:
-  "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A"
-  unfolding eq_def subset_def by blast
-
-lemma [code func]:
   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   unfolding subset_def Set.subset_def ..