diff -r 9f1eaab75e8c -r 771b1f6422a8 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/ZF/domrange.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -101,7 +101,7 @@
 
 qed_goalw "fieldCI" ZF.thy [field_def]
     "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
- (fn [prem]=> [ (blast_tac (!claset addIs [prem]) 1) ]);
+ (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
 
 qed_goalw "fieldE" ZF.thy [field_def]
      "[| a : field(r);  \
@@ -191,7 +191,7 @@
 AddIs  [vimageI];
 AddSEs [vimageE];
 
-val ZF_cs = !claset delrules [equalityI];
+val ZF_cs = claset() delrules [equalityI];
 
 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
 goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \