--- a/src/HOL/Hoare/List_Examples.ML Wed Jul 17 17:15:54 1996 +0200
+++ b/src/HOL/Hoare/List_Examples.ML Fri Jul 19 15:56:01 1996 +0200
@@ -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 HOL_cs);
+by(safe_tac (!claset));
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 HOL_cs);
+by(safe_tac (!claset));
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
qed "imperative_append";