--- a/Nominal/Ex/Multi_Recs2.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Ex/Multi_Recs2.thy	Wed May 25 21:38:50 2011 +0200
@@ -83,9 +83,6 @@
 thm fun_recs.fsupp
 thm fun_recs.supp
 
-
-
-
 lemma
   fixes c::"'a::fs"
   assumes "\<And>name c. P1 c (Var name)"
@@ -106,16 +103,21 @@
   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(simp_all)[1]
+  apply(blast)
   apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
-  apply(simp_all)[2]
+  apply(blast)
+  apply(blast)
   apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4))
-  apply(simp_all)[1]
+  apply(blast)
   apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5))
-  apply(simp_all)[2]
+  apply(blast)
+  apply(blast)
   apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6))
-  apply(simp_all)[3]
+  apply(blast)
+  apply(blast)
+  apply(blast)
   apply(tactic {* prove_termination_ind @{context} 1 *})
   apply(simp_all add: fun_recs.size)
   done