diff -r 84e1f8d8f30a -r ea93e088398d doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 16 20:02:11 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 16 20:27:35 2010 +0100
@@ -781,6 +781,28 @@
   \end{description}
 *}
 
+text %mlex {* The following simple examples demonstrate how to produce
+  fresh names from the initial @{ML Name.context}. *}
+
+ML {*
+  Name.invents Name.context "a" 5;
+  #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
+*}
+
+text {* \medskip The same works reletively to the formal context as
+follows. *}
+
+locale ex = fixes a b c :: 'a
+begin
+
+ML {*
+  val names = Variable.names_of @{context};
+  Name.invents names "a" 5;
+  #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
+*}
+
+end
+
 
 subsection {* Indexed names \label{sec:indexname} *}