doc-src/HOL/HOL.tex

--- a/doc-src/HOL/HOL.tex	Wed Mar 06 14:48:21 2002 +0100
+++ b/doc-src/HOL/HOL.tex	Wed Mar 06 16:18:45 2002 +0100
@@ -2782,11 +2782,13 @@
 
 constscode : 'consts_code' (codespec +);
 
-codespec : name ( () | '::' type) '(' mixfix ')';
+codespec : name ( () | '::' type) template;
 
 typescode : 'types_code' (tycodespec +);
 
-tycodespec : name '(' mixfix ')';
+tycodespec : name template;
+
+template: '(' string ')';
 \end{rail}
 \caption{Code generator syntax}
 \label{fig:HOL:codegen}