--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 19:21:07 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 19:21:14 2014 +0200
@@ -507,8 +507,8 @@
\item
The @{text "plugins"} option indicates which plugins should be enabled
-(@{text only}) or disabled (@{text del}). Wildcards (``@{text *}'') are allowed
-(e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
+(@{text only}) or disabled (@{text del}). Wildcards (``@{text "*"}'') are
+allowed (e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
\item
The @{text "discs_sels"} option indicates that discriminators and selectors