--- a/Tutorial/Lambda.thy	Wed Jan 19 19:41:50 2011 +0100
+++ b/Tutorial/Lambda.thy	Wed Jan 19 23:58:12 2011 +0100
@@ -4,6 +4,7 @@
 
 section {* Definitions for Lambda Terms *}
 
+
 text {* type of variables *}
 
 atom_decl name
@@ -50,7 +51,7 @@
   by (relation "measure size") (simp_all add: lam.size)
   
 
-subsection {* Capture-avoiding Substitution *}
+subsection {* Capture-Avoiding Substitution *}
 
 nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90,90,90] 90)
@@ -97,7 +98,7 @@
 done
 
 termination
-  by (relation "measure (\<lambda>(t,_,_). size t)")
+  by (relation "measure (\<lambda>(t, _, _). size t)")
      (simp_all add: lam.size)
 
 lemma subst_eqvt[eqvt]: