--- a/ProgTutorial/Essential.thy	Mon May 31 22:27:48 2010 +0200
+++ b/ProgTutorial/Essential.thy	Mon May 31 22:43:31 2010 +0200
@@ -983,13 +983,15 @@
   "let
   val trm_list = 
         [@{term_pat \"?X\"},              @{term_pat \"a\"},
-         @{term_pat \"\<lambda>a b. ?X a b\"},    @{term_pat \"\<lambda>a b. (op +) a b\"},
+         @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
+         @{term_pat \"\<lambda>a b. (op +) a b\"},
          @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
-         @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"}] 
+         @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
+         @{term_pat \"?X a\"}] 
 in
   map Pattern.pattern trm_list
 end"
-  "[true, true, true, true, true, false, false, false]"}
+  "[true, true, true, true, true, false, false, false, false]"}
 
   The point of the restriction to patterns is that unification and matching 
   are decidable and produce most general unifiers, respectively matchers.