# HG changeset patch
# User haftmann
# Date 1423137672 -3600
# Node ID 9b590e32646a5fa6e7b1302f7d2a70fb6e57e537
# Parent  74f638efffcb85cbfcf6c0380948cefdf8a7dddb
more explicit hint on import order

diff -r 74f638efffcb -r 9b590e32646a src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Thu Feb 05 13:01:12 2015 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Thu Feb 05 13:01:12 2015 +0100
@@ -148,7 +148,7 @@
   discretion of the user to take care for this.
 \<close>
 
-subsection \<open>Common adaptation patterns\<close>
+subsection \<open>Common adaptation applications\<close>
 
 text \<open>
   The @{theory HOL} @{theory Main} theory already provides a code
@@ -186,15 +186,17 @@
        containing both @{text "Code_Target_Nat"} and
        @{text "Code_Target_Int"}.
 
-    \item[@{text "Code_Char"}] represents @{text HOL} characters by
-       character literals in target languages.
-
     \item[@{theory "String"}] provides an additional datatype @{typ
        String.literal} which is isomorphic to strings; @{typ
        String.literal}s are mapped to target-language strings.  Useful
        for code setups which involve e.g.~printing (error) messages.
        Part of @{text "HOL-Main"}.
 
+    \item[@{text "Code_Char"}] represents @{text HOL} characters by
+       character literals in target languages.  \emph{Warning:} This
+       modifies adaptation in a non-conservative manner and thus
+       should always be imported \emph{last} in a theory header.
+
     \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
        isomorphic to lists but implemented by (effectively immutable)
        arrays \emph{in SML only}.