--- a/Nominal/Ex/Foo1.thy	Thu Dec 23 00:46:06 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Thu Dec 23 01:05:05 2010 +0000
@@ -73,8 +73,7 @@
   and     a9: "\<And>c. P3 c (BNil)"
   and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
   shows "P1 c t" "P2 c as" "P3 c as'"
-using assms
-apply(induction_schema)
+apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
 apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1))
 apply(simp_all)[7]
 apply(rule_tac ya="as"in foo.strong_exhaust(2))