diff -r 343a9888e875 -r ef2a6fdd3564 src/HOLCF/FOCUS/FOCUS.ML
--- a/src/HOLCF/FOCUS/FOCUS.ML	Sat Nov 03 18:42:38 2001 +0100
+++ b/src/HOLCF/FOCUS/FOCUS.ML	Sat Nov 03 18:42:55 2001 +0100
@@ -4,8 +4,6 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-open FOCUS;
-
 val ex_eqI = prove_goal thy "? xx. x = xx" (K [Auto_tac]);
 val ex2_eqI = prove_goal thy "? xx yy. x = xx & y = yy" (K [Auto_tac]);
 val eq_UU_symf = prove_goal thy "(UU = f x) = (f x = UU)" (K [Auto_tac]);