# HG changeset patch
# User haftmann
# Date 1307771428 -7200
# Node ID eaf8b7f22d3973fd69d352d70c64dc458a578ef9
# Parent  8d3a5b7b9a001c82eacaa1c1b166b90091b18829
tuned comment

diff -r 8d3a5b7b9a00 -r eaf8b7f22d39 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Fri Jun 10 17:52:09 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Sat Jun 11 07:50:28 2011 +0200
@@ -12,7 +12,7 @@
 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 Cset}.
+  type @{text Cset.set} from theory @{text Cset}.
 *}
 
 declare mem_def [code del]