--- a/Tutorial/Tutorial1.thy	Sat Jan 22 23:24:20 2011 -0600
+++ b/Tutorial/Tutorial1.thy	Tue Jan 25 02:42:15 2011 +0900
@@ -207,7 +207,7 @@
 *}
 
 inductive
-  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
+  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 60)
 where
   e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
 | e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"