# HG changeset patch
# User haftmann
# Date 1166426491 -3600
# Node ID 5df10a17644e319be77a3092b7d6ea770ea70b3d
# Parent  aa350df2372cb007d2859e0a4f418d8b7f3ce693
explicit nonfix declaration for ML "subset"

diff -r aa350df2372c -r 5df10a17644e src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Dec 18 08:21:30 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Dec 18 08:21:31 2006 +0100
@@ -271,6 +271,7 @@
 ML {*
 nonfix inter;
 nonfix union;
+nonfix subset;
 *}
 
 code_modulename SML