# HG changeset patch
# User haftmann
# Date 1372488304 -7200
# Node ID 7d7b4e285ea70d4c4d86d60b240e8e23aa85b4af
# Parent  445ae7a4e4e1a3b394562ce1cb646f80ac71fd60
yet another warning

diff -r 445ae7a4e4e1 -r 7d7b4e285ea7 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Jun 28 21:07:42 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Sat Jun 29 08:45:04 2013 +0200
@@ -2459,7 +2459,9 @@
   module names) with target-specific hints how these symbols shall be named.
   \emph{Warning:} These hints are still subject to name disambiguation.
   @{command (HOL) "code_modulename"} is a legacy variant for
-  @{command (HOL) "code_identifier"} on module names.
+  @{command (HOL) "code_identifier"} on module names.  It is at the discretion
+  of the user to ensure that name prefixes of identifiers in compound
+  statements like type classes or datatypes are still the same.
 
   \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
   argument compiles code into the system runtime environment and