diff -r e8732350a29f -r d1d09177ec89 Nominal/Ex/Height.thy
--- a/Nominal/Ex/Height.thy	Fri Dec 31 12:12:59 2010 +0000
+++ b/Nominal/Ex/Height.thy	Fri Dec 31 13:31:39 2010 +0000
@@ -14,7 +14,6 @@
   | App "lam" "lam"
   | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100)
 
-thm lam.strong_induct
 
 text {* Definition of the height-function on lambda-terms. *} 
 
@@ -84,17 +83,17 @@
 theorem height_subst:
   shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
-  case (1 y)
+  case (Var y)
   have "1 \<le> height e'" by (rule height_ge_one)
   then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
 next
-  case (3 y e1)
+  case (Lam y e1)
   have ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by fact
   moreover
   have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *)
   ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
 next    
-  case (2 e1 e2)
+  case (App e1 e2)
   have ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" 
   and  ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by fact+
   then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp