1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 17 18:10:35 2005 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 17 18:10:36 2005 +0200
     1.3 @@ -109,13 +109,13 @@
     1.4  This \verb!no_vars! business can become a bit tedious.
     1.5  If you would rather never see question marks, simply put
     1.6  \begin{verbatim}
     1.7 -reset show_var_qmarks;
     1.8 +reset show_question_marks;
     1.9  \end{verbatim}
    1.10  at the beginning of your file \texttt{ROOT.ML}.
    1.11  The rest of this document is produced with this flag reset.
    1.12  *}
    1.13  
    1.14 -(*<*)ML"reset show_var_qmarks"(*>*)
    1.15 +(*<*)ML"reset show_question_marks"(*>*)
    1.16  
    1.17  subsection "Inference rules"
    1.18  
    1.19 @@ -339,7 +339,7 @@
    1.20      \verb!    | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\
    1.21      \verb!    | my_lhs ctxt (_ $ t $ _) = t!\\
    1.22      \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
    1.23 -    \verb!  in [TermStyle.update_style "new_lhs" my_lhs]!\\
    1.24 +    \verb!  in [TermStyle.add_style "new_lhs" my_lhs]!\\
    1.25      \verb!end;!\\
    1.26      \verb!*!\verb!}!\\
    1.27    \end{quote}