diff -r 659707452f55 -r 55e83c32cdec doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Wed Jun 09 15:00:32 2004 +0200
+++ b/doc-src/Ref/defining.tex	Wed Jun 09 18:50:38 2004 +0200
@@ -494,25 +494,6 @@
   "-" :: exp => exp          ("- _"    [3] 3)
 end
 \end{ttbox}
-If you put this into a file {\tt ExpSyntax.thy} and load it by {\tt
-  use_thy"ExpSyntax"}, you can run some tests:
-\begin{ttbox}
-val read_exp = Syntax.test_read (syn_of ExpSyntax.thy) "exp";
-{\out val it = fn : string -> unit}
-read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
-{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
-{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
-{\out \vdots}
-read_exp "0 + - 0 + 0";
-{\out tokens: "0" "+" "-" "0" "+" "0"}
-{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
-{\out \vdots}
-\end{ttbox}
-The output of \ttindex{Syntax.test_read} includes the token list ({\tt
-  tokens}) and the raw \AST{} directly derived from the parse tree,
-ignoring parse \AST{} translations.  The rest is tracing information
-provided by the macro expander (see \S\ref{sec:macros}).
-
 Executing {\tt Syntax.print_gram} reveals the productions derived from the
 above mixfix declarations (lots of additional information deleted):
 \begin{ttbox}