--- a/src/HOL/Relation.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Relation.ML Mon Nov 03 12:13:18 1997 +0100
@@ -178,11 +178,11 @@
(REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
goal Relation.thy "R O id = R";
-by (fast_tac (!claset addbefore split_all_tac) 1);
+by (fast_tac (claset() addbefore split_all_tac) 1);
qed "R_O_id";
goal Relation.thy "id O R = R";
-by (fast_tac (!claset addbefore split_all_tac) 1);
+by (fast_tac (claset() addbefore split_all_tac) 1);
qed "id_O_R";
Addsimps [R_O_id,id_O_R];