--- a/src/HOL/Isar_examples/HoareEx.thy	Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Dec 19 16:32:14 2007 +0100
@@ -39,7 +39,7 @@
 *}
 
 lemma
-  "|- .{\<acute>(N_update (K_record (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+  "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
   by (rule assign)
 
 text {*