diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Option.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -82,13 +82,13 @@
 
 
 Goal "x : o2s xo = (xo = Some x)";
-by (exhaust_tac "xo" 1);
+by (cases_tac "xo" 1);
 by Auto_tac;
 qed "elem_o2s";
 AddIffs [elem_o2s];
 
 Goal "(o2s xo = {}) = (xo = None)";
-by (exhaust_tac "xo" 1);
+by (cases_tac "xo" 1);
 by Auto_tac;
 qed "o2s_empty_eq";