diff -r edd5a2ea3807 -r 0cab06e3bbd0 src/HOLCF/FOCUS/Buffer.ML
--- a/src/HOLCF/FOCUS/Buffer.ML	Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML	Thu Aug 28 01:56:40 2003 +0200
@@ -247,7 +247,7 @@
 Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
 by Safe_tac;
 by (EVERY'[rename_tac "f", res_inst_tac 
-        [("x","\\<lambda>s. case s of Sd d => \\<Lambda>x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
+        [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
 by ( Simp_tac 1);
 by (etac weak_coinduct_image 1);
 by (rewtac BufSt_F_def);