diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/IMP/Transition.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -220,7 +220,7 @@
 by (Clarify_tac 1);
 by (etac rel_pow_E2 1);
  by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
-by (exhaust_tac "c" 1);
+by (cases_tac "c" 1);
     by (fast_tac (claset() addSDs [hlemma]) 1);
    by (Blast_tac 1);
   by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);