--- a/ProgTutorial/General.thy	Tue Nov 10 12:17:08 2009 +0100
+++ b/ProgTutorial/General.thy	Wed Nov 11 05:34:46 2009 +0100
@@ -1013,18 +1013,18 @@
   the latter @{ML_ind unify in Pattern} both implemented in the structure
   @{ML_struct Pattern}. An example for higher-order pattern unification is
 
-  \ldots
-*}
-
-ML{*let
-  val pat = @{term_pat "?X"}
-  val trm = @{term "a"}
-  val init = (Vartab.empty, Vartab.empty)
+  @{ML_response_fake [display, gray]
+  "let
+  val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
+  val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
+  val init = Envir.empty 0
+  val env = Pattern.unify @{theory} (trm1, trm2) init
 in
-  Pattern.match @{theory} (pat, trm) init
-end *}
-
-text {*
+  pretty_env @{context} (Envir.term_env env)
+end"
+  "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
+
+
   An assumption of this function is that the terms to be unified have 
   already the same type. In case of failure, the exceptions that are raised
   are either @{text Pattern}, @{text MATCH} or @{text Unif}.