--- a/src/HOL/BCV/Machine.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Machine.ML Mon Mar 13 12:51:10 2000 +0100
@@ -68,15 +68,15 @@
by (Blast_tac 2);
by (etac thin_rl 1);
by (asm_full_simp_tac (simpset() addsimps [le_typ])1);
-by (exhaust_tac "t!nat1" 1);
+by (cases_tac "t!nat1" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "s!nat1" 1);
+by (cases_tac "s!nat1" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "exec_mono_None";