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