diff -r 8812a07d52ee -r 96722b04f2ae doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sat Jul 01 19:56:46 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Sat Jul 01 19:58:59 2000 +0200
@@ -300,6 +300,7 @@
 
 \indexisaratt{standard}
 \indexisaratt{elimify}
+\indexisaratt{no-vars}
 
 \indexisaratt{RS}\indexisaratt{COMP}
 \indexisaratt{where}
@@ -316,6 +317,7 @@
   fold & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
   elimify & : & \isaratt \\
+  no_vars & : & \isaratt \\
   export^* & : & \isaratt \\
 \end{matharray}
 
@@ -356,6 +358,9 @@
 \item [$elimify$] turns an destruction rule into an elimination, just as the
   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   
+\item [$no_vars$] replaces schematic variables by free ones; this is mainly
+  for tuning output of pretty printed theorems.
+  
 \item [$export$] lifts a local result out of the current proof context,
   generalizing all fixed variables and discharging all assumptions.  Note that
   proper incremental export is already done as part of the basic Isar