diff -r f7a5e06adea1 -r 8f9056ce5dfb src/HOL/Lambda/ListOrder.ML
--- a/src/HOL/Lambda/ListOrder.ML	Mon Aug 17 13:09:08 1998 +0200
+++ b/src/HOL/Lambda/ListOrder.ML	Mon Aug 17 13:09:40 1998 +0200
@@ -83,7 +83,7 @@
 AddSIs [Cons_acc_step1I];
 
 Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
-be lists.induct 1;
+by (etac lists.induct 1);
  by (rtac accI 1);
  by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
 by (rtac accI 1);