diff -r 5de99514fd07 -r 2d399a776de2 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Dec 25 08:42:33 2011 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 17:40:43 2011 +0100
@@ -9,7 +9,7 @@
   "../JVM/JVMListExample"
   BVSpecTypeSafe
   JVM
-  "~~/src/HOL/Library/Executable_Set"
+  "~~/src/HOL/Library/More_Set"
 begin
 
 text {*
@@ -437,7 +437,6 @@
   "some_elem = (%S. SOME x. x : S)"
 code_const some_elem
   (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
-setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *}
 
 text {* This code setup is just a demonstration and \emph{not} sound! *}