diff -r f7a5e06adea1 -r 8f9056ce5dfb src/HOL/Lambda/ListBeta.ML
--- a/src/HOL/Lambda/ListBeta.ML	Mon Aug 17 13:09:08 1998 +0200
+++ b/src/HOL/Lambda/ListBeta.ML	Mon Aug 17 13:09:40 1998 +0200
@@ -6,7 +6,7 @@
 
 Goal
  "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
-be beta.induct 1;
+by (etac beta.induct 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
 by (res_inst_tac [("xs","rs")] rev_exhaust 1);
@@ -28,7 +28,7 @@
 \     ( (? r'. r -> r' & u' = r'$$rs) | \
 \       (? rs'. rs => rs' & u' = r$$rs') | \
 \       (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
-be beta.induct 1;
+by (etac beta.induct 1);
    by (clarify_tac (claset() delrules [disjCI]) 1);
    by (exhaust_tac "r" 1);
      by (Asm_full_simp_tac 1);