--- a/Nominal/Ex/Multi_Recs2.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -69,34 +69,6 @@
 thm fun_recs.fsupp
 thm fun_recs.supp
 
-term alpha_b_fnclause
-term alpha_b_fnclauses
-term alpha_b_lrb
-term alpha_b_lrbs
-term alpha_b_pat
-
-term alpha_b_fnclause_raw
-term alpha_b_fnclauses_raw
-term alpha_b_lrb_raw
-term alpha_b_lrbs_raw
-term alpha_b_pat_raw
-
-lemma uu1:
-  fixes as0::exp  and as1::fnclause
-  shows "(\<lambda>x::exp. True) (as0::exp)"
-  and   "alpha_b_fnclause as1 (permute_b_fnclause p as1)"
-  and   "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)"
-  and   "alpha_b_lrb as3 (permute_b_lrb p as3)"
-  and   "alpha_b_lrbs as4 (permute_b_lrbs p as4)"
-  and   "alpha_b_pat as5 (permute_b_pat p as5)"
-apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts)
-apply(simp_all)
-apply(simp only: fun_recs.perm_bn_simps)
-apply(simp only: fun_recs.eq_iff)
-apply(simp)
-oops
-
-
 thm fun_recs.distinct
 thm fun_recs.induct
 thm fun_recs.inducts