doc-src/LaTeXsugar/Sugar/Sugar.thy
changeset 18708 4b3dadb4fe33
parent 17127 65e340b6a56f
child 21558 63278052bb72
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Jan 19 15:45:10 2006 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Jan 19 21:22:08 2006 +0100
@@ -389,7 +389,7 @@
 setup {*
 let
   fun my_concl ctxt = Logic.strip_imp_concl
-  in [TermStyle.add_style "my_concl" my_concl]
+  in TermStyle.add_style "my_concl" my_concl
 end;
 *}
 (*>*)
@@ -399,7 +399,7 @@
     \verb!setup {!\verb!*!\\
     \verb!let!\\
     \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
-    \verb!  in [TermStyle.add_style "my_concl" my_concl]!\\
+    \verb!  in TermStyle.add_style "my_concl" my_concl!\\
     \verb!end;!\\
     \verb!*!\verb!}!\\
   \end{quote}