--- a/src/HOL/Nominal/Examples/Height.thy Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy Thu May 22 16:34:41 2008 +0200
@@ -49,7 +49,7 @@
lemma height_ge_one:
shows "1 \<le> (height e)"
-by (nominal_induct e rule: lam.induct) (simp_all)
+by (nominal_induct e rule: lam.strong_induct) (simp_all)
text {*
Unlike the proplem suggested by Wang, however, the
@@ -58,7 +58,7 @@
theorem height_subst:
shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
-proof (nominal_induct e avoiding: x e' rule: lam.induct)
+proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
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