src/HOL/MicroJava/BV/BVExample.thy

--- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -433,7 +433,7 @@
 qed
 
 definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
-  "some_elem = (%S. SOME x. x : S)"
+  "some_elem = (\<lambda>S. SOME x. x \<in> S)"
 code_printing
   constant some_elem \<rightharpoonup> (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"
 
@@ -486,4 +486,3 @@
 \<close>
 
 end
-