--- a/src/Doc/Codegen/Adaptation.thy Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Adaptation.thy Mon Jan 14 18:33:53 2019 +0000
@@ -232,7 +232,7 @@
| constant HOL.conj \<rightharpoonup> (SML)
| constant Not \<rightharpoonup> (SML)
(*>*)
-text %quotetypewriter \<open>
+text %quote \<open>
@{code_stmts in_interval (SML)}
\<close>
@@ -262,7 +262,7 @@
placeholder for the constant's or the type constructor's arguments.
\<close>
-text %quotetypewriter \<open>
+text %quote \<open>
@{code_stmts in_interval (SML)}
\<close>
@@ -277,7 +277,7 @@
code_printing %quotett
constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
-text %quotetypewriter \<open>
+text %quote \<open>
@{code_stmts in_interval (SML)}
\<close>