--- a/Tutorial/Tutorial5.thy	Sat Jan 22 16:36:21 2011 -0600
+++ b/Tutorial/Tutorial5.thy	Sat Jan 22 16:37:00 2011 -0600
@@ -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!