--- a/src/HOL/Set.thy Thu Nov 08 22:57:45 2007 +0100
+++ b/src/HOL/Set.thy Fri Nov 09 13:41:27 2007 +0100
@@ -2255,6 +2255,7 @@
"Union A = UNION A (\<lambda>x. x)"
by auto
+code_reserved SML union inter (* Avoid clashes with ML infixes *)
subsection {* Basic ML bindings *}