diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -90,7 +90,7 @@
 
 lemma Cons_acc_step1I [intro!]:
     "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
-  apply (induct fixing: xs set: acc)
+  apply (induct arbitrary: xs set: acc)
   apply (erule thin_rl)
   apply (erule acc_induct)
   apply (rule accI)