--- a/src/HOL/Lambda/WeakNorm.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Mon Sep 11 21:35:19 2006 +0200
@@ -114,7 +114,7 @@
by (induct ts) simp_all
lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
- apply (induct fixing: i j set: NF)
+ apply (induct arbitrary: i j set: NF)
apply simp
apply (frule listall_conj1)
apply (drule listall_conj2)
@@ -156,7 +156,7 @@
by (induct ts) simp_all
lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
- apply (induct fixing: i set: NF)
+ apply (induct arbitrary: i set: NF)
apply (frule listall_conj1)
apply (drule listall_conj2)
apply (drule_tac i=i in lift_terms_NF)