# HG changeset patch
# User haftmann
# Date 1283627439 -7200
# Node ID 5ec8e4404c3309483c0bfe64cae4c4b8e6c5d4c2
# Parent  7430f17fd80e2ed5ee865999ae3eb0b2505af35f
added more explicit warning

diff -r 7430f17fd80e -r 5ec8e4404c33 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Fri Sep 03 08:13:28 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Sat Sep 04 21:10:39 2010 +0200
@@ -9,6 +9,12 @@
 imports More_Set
 begin
 
+text {*
+  This is just an ad-hoc hack which will rarely give you what you want.
+  For the moment, whenever you need executable sets, consider using
+  type @{text fset} from theory @{text Fset}.
+*}
+
 declare mem_def [code del]
 declare Collect_def [code del]
 declare insert_code [code del]