| changeset 20503 | 503ac4c5ef91 |
| parent 19564 | d3e2f532459a |
| child 21404 | eb85850d3eb7 |
--- 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)