# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID c1507d5f46654d74278e00363b2b458e799e625b
# Parent  b0126a5a256db3338cc63e2cb21c54f1354cd6d3
tuned doc comment

diff -r b0126a5a256d -r c1507d5f4665 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -2708,8 +2708,6 @@
 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
 %
 % *names of variables suboptimal
-%
-% * in a locale, size is half broken
 *}
 *)