--- a/src/Doc/IsarImplementation/Prelim.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy Sun Mar 02 19:00:45 2014 +0100
@@ -709,7 +709,7 @@
of declared type and term variable names. Projecting a proof
context down to a primitive name context is occasionally useful when
invoking lower-level operations. Regular management of ``fresh
- variables'' is done by suitable operations of structure @{ML_struct
+ variables'' is done by suitable operations of structure @{ML_structure
Variable}, which is also able to provide an official status of
``locally fixed variable'' within the logical environment (cf.\
\secref{sec:variables}).