diff -r 8eb32cd3122e -r ae28c198e78d src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Fri Mar 10 23:04:07 2000 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Mon Mar 13 09:08:27 2000 +0100
@@ -183,7 +183,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (exhaust_tac "k" 1),
+        (cases_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -220,7 +220,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (exhaust_tac "k" 1),
+        (cases_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -381,7 +381,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (exhaust_tac "k" 1),
+        (cases_tac "k" 1),
         (hyp_subst_tac 1),
         (strip_tac 1),
         (Simp_tac 1),
@@ -410,7 +410,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (exhaust_tac "k" 1),
+        (cases_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),