--- a/src/HOLCF/Discrete.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Discrete.ML Mon Nov 03 14:06:27 1997 +0100
@@ -11,10 +11,10 @@
goal thy
"!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
-by(fast_tac (!claset addDs [discr_chain0] addEs [arg_cong]) 1);
+by(fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
-by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
+by(simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
qed "cont_discr";
AddIffs [cont_discr];