diff -r 984ea1299cd7 -r 0b21101157b1 Nominal/TySch.thy
--- a/Nominal/TySch.thy	Fri Mar 19 08:31:43 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 09:03:10 2010 +0100
@@ -59,12 +59,20 @@
 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
 
 lemma induct:
-"\<lbrakk>\<And>name b. P b (Var name);
-  \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2);
-  \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)
- \<rbrakk> \<Longrightarrow> P a t"
-  oops
-
+  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"
+proof -
+  have "\<And>p. P a (p \<bullet> t)"
+    apply (induct t rule: t_tyS.inducts(1))
+    apply (simp add: a1)
+    apply (simp_all)
+    apply (rule_tac ?t1.0="p \<bullet> t1" and ?t2.0="p \<bullet> t2" in a2)
+    sorry
+  then have "P a (0 \<bullet> t)" by blast
+  then show "P a t" by simp
+qed
 
 lemma
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"