--- a/src/HOL/Hoare/List_Examples.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Hoare/List_Examples.ML Wed Nov 05 13:23:46 1997 +0100
@@ -8,7 +8,7 @@
\{y=rev(X)}";
by (hoare_tac 1);
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "imperative_reverse";
@@ -23,7 +23,7 @@
\{y = X@Y}";
by (hoare_tac 1);
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "imperative_append";