--- a/src/Doc/IsarRef/Generic.thy Fri May 17 20:41:45 2013 +0200
+++ b/src/Doc/IsarRef/Generic.thy Fri May 17 20:53:28 2013 +0200
@@ -31,7 +31,7 @@
``global'', which may not be changed within a local context.
\begin{matharray}{rcll}
- @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@{rail "
@@ -40,7 +40,7 @@
\begin{description}
- \item @{command "print_configs"} prints the available configuration
+ \item @{command "print_options"} prints the available configuration
options, with names, types, and current values.
\item @{text "name = value"} as an attribute expression modifies the