--- a/src/ZF/ex/Primrec0.ML Thu Nov 18 14:57:05 1993 +0100
+++ b/src/ZF/ex/Primrec0.ML Thu Nov 18 18:48:23 1993 +0100
@@ -337,7 +337,7 @@
by (etac List.elim 1);
by (asm_simp_tac (ack2_ss addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
by (asm_simp_tac ack2_ss 1);
-be ssubst 1; (*get rid of the needless assumption*)
+by (etac ssubst 1); (*get rid of the needless assumption*)
by (eres_inst_tac [("n","a")] nat_induct 1);
(*base case*)
by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,