--- a/src/HOL/Hoare/List_Examples.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Hoare/List_Examples.ML Mon Nov 03 12:13:18 1997 +0100
@@ -7,8 +7,8 @@
\ END \
\{y=rev(X)}";
by (hoare_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
-by (safe_tac (!claset));
+by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
+by (safe_tac (claset()));
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "imperative_reverse";
@@ -22,8 +22,8 @@
\ END \
\{y = X@Y}";
by (hoare_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
-by (safe_tac (!claset));
+by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
+by (safe_tac (claset()));
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "imperative_append";