diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Discrete.ML
--- a/src/HOLCF/Discrete.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Discrete.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -10,11 +10,11 @@
 Addsimps [undiscr_Discr];
 
 goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i.f(S i)) = {f(S 0)}";
+ "!!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);
 qed "discr_chain_f_range0";
 
-goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr.f x)";
+goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
 by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
 qed "cont_discr";
 AddIffs [cont_discr];