--- 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! *}