# HG changeset patch
# User haftmann
# Date 1160722941 -7200
# Node ID 330a8a6dd53ce554f52e4acb53aaa6f125c11348
# Parent  1bbb31aaf98dc00124d4f40f2b7967f574ec4a9d
explicit nonfix for union and inter

diff -r 1bbb31aaf98d -r 330a8a6dd53c src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Thu Oct 12 22:57:45 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Oct 13 09:02:21 2006 +0200
@@ -230,6 +230,11 @@
 
 section {* code generator setup *}
 
+ML {*
+nonfix inter;
+nonfix union;
+*}
+
 code_constname
   "ExecutableSet.member" "List.member"
   "ExecutableSet.insertl" "List.insertl"