diff -r 3bbe7cab8037 -r 65a9a30b8ece src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Tue Oct 10 15:33:25 2006 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Tue Oct 10 16:26:59 2006 +0200
@@ -212,6 +212,9 @@
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<lless> \<Gamma>2"
   shows "\<Gamma>2 \<turnstile> t:\<sigma>"
+
+thm typing.induct[no_vars]
+
 using a b c
 proof (induct arbitrary: \<Gamma>2)
   case (t1 \<Gamma>1 \<tau> a) (* variable case *)