--- a/Nominal/Ex/Multi_Recs2.thy Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy Tue Dec 07 14:27:39 2010 +0000
@@ -50,7 +50,7 @@
| "b_fnclause (K x pat exp) = {atom x}"
-
+thm fun_recs.permute_bn
thm fun_recs.perm_bn_alpha
thm fun_recs.perm_bn_simps
thm fun_recs.bn_finite