diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListOrder.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -87,18 +87,17 @@
   apply blast
   done
 
-lemma Cons_acc_step1I [rule_format, intro!]:
-    "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
-  apply (erule acc_induct)
+lemma Cons_acc_step1I [intro!]:
+    "x \<in> acc r ==> (!!xs. xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r))"
+  apply (induct set: acc)
   apply (erule thin_rl)
-  apply clarify
   apply (erule acc_induct)
   apply (rule accI)
   apply blast
   done
 
 lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
-  apply (erule lists.induct)
+  apply (induct set: lists)
    apply (rule accI)
    apply simp
   apply (rule accI)
@@ -114,7 +113,7 @@
   done
 
 lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
-  apply (erule acc_induct)
+  apply (induct set: acc)
   apply clarify
   apply (rule accI)
   apply (drule ex_step1I, assumption)