diff -r 4b4742aa43f2 -r 11f6a561eb4b Nominal/Ex/Multi_Recs2.thy
--- a/Nominal/Ex/Multi_Recs2.thy	Sat Dec 17 17:03:01 2011 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Sat Dec 17 17:08:47 2011 +0000
@@ -83,44 +83,6 @@
 thm fun_recs.fsupp
 thm fun_recs.supp
 
-lemma
-  fixes c::"'a::fs"
-  assumes "\<And>name c. P1 c (Var name)"
-  and "\<And>c. P1 c Unit"
-  and "\<And>exp1 exp2 c. \<lbrakk>\<And>c. P1 c exp1; \<And>c. P1 c exp2\<rbrakk> \<Longrightarrow> P1 c (Multi_Recs2.Pair exp1 exp2)"
-  and "\<And>lrbs exp c. \<lbrakk>b_lrbs lrbs \<sharp>* c; \<And>c. P5 c lrbs; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P1 c (LetRec lrbs exp)"
-  and "\<And>name pat exp c. \<lbrakk>b_pat pat \<sharp>* c; \<And>c. P6 c pat; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P2 c (K name pat exp)"
-  and "\<And>fnclause c. (\<And>c. P2 c fnclause) \<Longrightarrow> P3 c (S fnclause)"
-  and "\<And>fnclause fnclauses c. \<lbrakk>\<And>c. P2 c fnclause; \<And>c. P3 c fnclauses\<rbrakk> \<Longrightarrow> 
-    P3 c (ORs fnclause fnclauses)"
-  and "\<And>fnclauses c. (\<And>c. P3 c fnclauses) \<Longrightarrow> P4 c (Clause fnclauses)"
-  and "\<And>lrb c. (\<And>c. P4 c lrb) \<Longrightarrow> P5 c (Single lrb)"
-  and "\<And>lrb lrbs c. \<lbrakk>\<And>c. P4 c lrb; \<And>c. P5 c lrbs\<rbrakk> \<Longrightarrow> P5 c (More lrb lrbs)"
-  and "\<And>name c. P6 c (PVar name)"
-  and "\<And>c. P6 c PUnit"
-  and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"
-  shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"
-  apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
-  apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))
-  apply(simp_all)[4]
-  apply(blast)
-  apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))
-  apply(blast)
-  apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
-  apply(blast)
-  apply(blast)
-  apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4))
-  apply(blast)
-  apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5))
-  apply(blast)
-  apply(blast)
-  apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6))
-  apply(blast)
-  apply(blast)
-  apply(blast)
-  apply(tactic {* prove_termination_ind @{context} 1 *})
-  apply(simp_all add: fun_recs.size)
-  done
 
 end