--- 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);