src/HOL/MicroJava/BV/BVExample.thy

--- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -434,8 +434,8 @@
 
 definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
   "some_elem = (%S. SOME x. x : S)"
-code_const some_elem
-  (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
+code_printing
+  constant some_elem \<rightharpoonup> (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"
 
 text {* This code setup is just a demonstration and \emph{not} sound! *}