--- a/ProgTutorial/First_Steps.thy	Wed Nov 02 13:38:19 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Thu Nov 03 17:53:36 2011 +0000
@@ -147,7 +147,7 @@
   for example:
 
   @{ML_response_fake [display,gray] 
-  "if 0=1 then true else (error \"foo\")" 
+  "if 0 = 1 then true else (error \"foo\")" 
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
@@ -645,6 +645,30 @@
   "acc_incs 1 ||>> (fn x => (x, x + 2))"
   "(((((\"\", 1), 2), 3), 4), 6)"}
 
+  An example where this combinator is useful is as follows
+
+  @{ML_response_fake [display, gray]
+  "let
+  val ((names1, names2), _) =
+    @{context}
+    |> Variable.variant_fixes (replicate 4 \"x\")
+    ||>> Variable.variant_fixes (replicate 5 \"x\")
+in
+  (names1, names2)
+end"
+  "([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"}
+
+  Its purpose is to create nine variants of the string @{ML "\"x\""} so
+  that no variant will clash with another. Suppose for some reason we want
+  to bind four variants to the lists @{ML_text "name1"} and the
+  rest to @{ML_text "name2"}. In order to obtain non-clashing
+  variants we have to thread the context through the function calls
+  (the context records which variants have been previously created).
+  For the first call we can use @{ML "|>"}, but in the
+  second and any further call to @{ML_ind variant_fixes in Variable} we 
+  have to use @{ML "||>>"} in order to account for the result(s) 
+  obtained by previous calls.
+  
   A more realistic example for this combinator is the following code
 *}
 
@@ -672,7 +696,6 @@
 end"
   "one
 one \<equiv> 1"}
-
   Recall that @{ML "|>"} is the reverse function application. Recall also that
   the related reverse function composition is @{ML "#>"}. In fact all the
   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}