--- a/Tutorial/Tutorial5.thy	Sun Jan 23 07:17:35 2011 +0900
+++ b/Tutorial/Tutorial5.thy	Sun Jan 23 07:32:28 2011 +0900
@@ -132,7 +132,7 @@
   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
 using a
 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
-   (auto elim: canonical_tArr)
+   (auto elim: canonical_tArr simp add: val.simps)
 
 text {*
   Done! Congratulations!