diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -18,7 +18,7 @@
   by blast
 
 lemma [code func]:
-  "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
+  "Code_Generator.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
   unfolding eq_def by blast
 
 declare bex_triv_one_point1 [symmetric, standard, code]