diff -r b4dcc32310fb -r d16d7ddcc842 src/HOL/Isar_examples/Cantor.ML
--- a/src/HOL/Isar_examples/Cantor.ML	Mon Aug 23 15:27:27 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.ML	Mon Aug 23 15:30:26 1999 +0200
@@ -2,14 +2,14 @@
 (* tactic script -- single steps *)
 
 Goal "EX S. S ~: range(f :: 'a => 'a set)";
-  br exI 1;
-  br notI 1;
-  be rangeE 1;
-  be equalityCE 1;
-  bd CollectD 1;
+  by (rtac exI 1);
+  by (rtac notI 1);
+  by (etac rangeE 1);
+  by (etac equalityCE 1);
+  by (dtac CollectD 1);
   by (contr_tac 1);
   by (swap_res_tac [CollectI] 1);
-  ba 1;
+  by (assume_tac 1);
 qed "it";