# HG changeset patch
# User wenzelm
# Date 1116346236 -7200
# Node ID a53abeedc8796f49aec5b4a9402755340662b0c9
# Parent  9d7f3db40b886ac1c097101302d530055d652f5e
renamed show_var_qmarks to show_question_marks;

diff -r 9d7f3db40b88 -r a53abeedc879 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 17 18:10:35 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 17 18:10:36 2005 +0200
@@ -109,13 +109,13 @@
 This \verb!no_vars! business can become a bit tedious.
 If you would rather never see question marks, simply put
 \begin{verbatim}
-reset show_var_qmarks;
+reset show_question_marks;
 \end{verbatim}
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag reset.
 *}
 
-(*<*)ML"reset show_var_qmarks"(*>*)
+(*<*)ML"reset show_question_marks"(*>*)
 
 subsection "Inference rules"
 
@@ -339,7 +339,7 @@
     \verb!    | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\
     \verb!    | my_lhs ctxt (_ $ t $ _) = t!\\
     \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
-    \verb!  in [TermStyle.update_style "new_lhs" my_lhs]!\\
+    \verb!  in [TermStyle.add_style "new_lhs" my_lhs]!\\
     \verb!end;!\\
     \verb!*!\verb!}!\\
   \end{quote}