--- a/src/HOL/Lambda/ListOrder.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/ListOrder.ML Mon Mar 13 12:51:10 2000 +0100
@@ -30,7 +30,7 @@
by (rtac iffI 1);
by (etac exE 1);
by (rename_tac "ts" 1);
- by (exhaust_tac "ts" 1);
+ by (cases_tac "ts" 1);
by (Force_tac 1);
by (Force_tac 1);
by (etac disjE 1);
@@ -51,7 +51,7 @@
\ !y. ys = y#xs --> (y,x) : r --> R; \
\ !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
\ |] ==> R";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
by (Blast_tac 1);
val lemma = result();