--- a/Nominal/Ex/TypeSchemes.thy	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Dec 28 19:51:25 2010 +0000
@@ -38,7 +38,7 @@
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
 thm tys2.distinct
-thm tys2.induct
+thm tys2.induct tys2.strong_induct
 thm tys2.exhaust tys2.strong_exhaust
 thm tys2.fv_defs
 thm tys2.bn_defs
@@ -50,18 +50,6 @@
 thm tys2.supp
 thm tys2.fresh
 
-lemma strong_induct:
-  fixes c::"'a::fs"
-  assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)"
-  shows "P c tys"
-using assms
-apply(induction_schema)
-apply(rule_tac y="tys" in tys2.strong_exhaust)
-apply(blast)
-apply(relation "measure (\<lambda>(x,y). size y)")
-apply(simp_all add: tys2.size)
-done
-
 
 text {* Some Tests *}