--- a/ProgTutorial/FirstSteps.thy	Fri Dec 04 23:45:32 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sun Dec 06 14:26:14 2009 +0100
@@ -842,7 +842,7 @@
   and the second is a proof. For example
 *}
 
-ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *}
+ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
 
 text {*
   The result can be printed out as follows.