separate quote tag from tt tag

--- a/doc-src/Codegen/Thy/Adaptation.thy	Fri Sep 24 15:53:57 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Fri Sep 24 16:09:54 2010 +0200
@@ -190,9 +190,9 @@
   "bool"}, we may use \qn{custom serialisations}:
 *}
 
-code_type %quotett bool
+code_type %quote %tt bool
   (SML "bool")
-code_const %quotett True and False and "op \<and>"
+code_const %quote %tt True and False and "op \<and>"
   (SML "true" and "false" and "_ andalso _")
 
 text {*
@@ -218,7 +218,7 @@
   precedences which may be used here:
 *}
 
-code_const %quotett "op \<and>"
+code_const %quote %tt "op \<and>"
   (SML infixl 1 "andalso")
 
 text %quote %typewriter {*
@@ -247,9 +247,9 @@
 code_const %invisible Pair
   (SML)
 (*>*)
-code_type %quotett prod
+code_type %quote %tt prod
   (SML infix 2 "*")
-code_const %quotett Pair
+code_const %quote %tt Pair
   (SML "!((_),/ (_))")
 
 text {*
@@ -283,10 +283,10 @@
   @{command_def code_class}) and its operation @{const [source] HOL.equal}
 *}
 
-code_class %quotett equal
+code_class %quote %tt equal
   (Haskell "Eq")
 
-code_const %quotett "HOL.equal"
+code_const %quote %tt "HOL.equal"
   (Haskell infixl 4 "==")
 
 text {*
@@ -307,7 +307,7 @@
 
 end %quote (*<*)
 
-(*>*) code_type %quotett bar
+(*>*) code_type %quote %tt bar
   (Haskell "Integer")
 
 text {*
@@ -316,7 +316,7 @@
   suppress this additional instance, use @{command_def "code_instance"}:
 *}
 
-code_instance %quotett bar :: equal
+code_instance %quote %tt bar :: equal
   (Haskell -)
 
 
@@ -328,10 +328,10 @@
   "code_include"} command:
 *}
 
-code_include %quotett Haskell "Errno"
+code_include %quote %tt Haskell "Errno"
 {*errno i = error ("Error number: " ++ show i)*}
 
-code_reserved %quotett Haskell Errno
+code_reserved %quote %tt Haskell Errno
 
 text {*
   \noindent Such named @{text include}s are then prepended to every

--- a/doc-src/Codegen/style.sty	Fri Sep 24 15:53:57 2010 +0200
+++ b/doc-src/Codegen/style.sty	Fri Sep 24 16:09:54 2010 +0200
@@ -37,9 +37,8 @@
 \renewcommand{\isatagtypewriter}{\begin{typewriter}}
 \renewcommand{\endisatagtypewriter}{\end{typewriter}}
 
-\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quote}}
+\isakeeptag{tt}
+\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
 
 %% a trick
 \newcommand{\isasymSML}{SML}