--- a/Nominal/TySch.thy	Fri Mar 19 09:03:10 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 09:31:38 2010 +0100
@@ -61,17 +61,22 @@
 lemma induct:
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
-  and     a3: "\<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
-  shows "P a t"
+  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
+  shows "P a t \<and> P' d ts "
 proof -
-  have "\<And>p. P a (p \<bullet> t)"
-    apply (induct t rule: t_tyS.inducts(1))
+  have " (\<forall>p. P a (p \<bullet> t)) \<and> (\<forall>p. P' d (p \<bullet> ts))"
+    apply (rule t_tyS.induct)
     apply (simp add: a1)
     apply (simp_all)
-    apply (rule_tac ?t1.0="p \<bullet> t1" and ?t2.0="p \<bullet> t2" in a2)
+    apply (rule allI)
+    apply (rule a2)
+    defer defer
+    apply (rule allI)
+    apply (rule a3)
+    apply simp_all
     sorry
-  then have "P a (0 \<bullet> t)" by blast
-  then show "P a t" by simp
+  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
+  then show ?thesis by simp
 qed
 
 lemma