# HG changeset patch
# User krauss
# Date 1194612087 -3600
# Node ID b8251517f50893d13a0ba7d3757a47495a313882
# Parent  96202af17d2bf2f2365db798380511292f39ece3
avoid name clashes when generating code for union, inter

diff -r 96202af17d2b -r b8251517f508 src/HOL/Set.thy
--- 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 *}