src/HOL/Set.thy

 
 lemma Union_code [code func]:
   "Union A = UNION A (\<lambda>x. x)"
   by auto
 
+code_reserved SML union inter (* Avoid clashes with ML infixes *)
 
 subsection {* Basic ML bindings *}
 
 ML {*
 val Ball_def = @{thm Ball_def}