diff -r 5f462dfaf130 -r 5c7a69cef18b ex/set.ML
--- a/ex/set.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/set.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -109,7 +109,7 @@
 by (fast_tac (set_cs addEs  [inj_ontoD, f_eq_gE]) 1);
 val bij_if_then_else = result();
 
-goal Lfp.thy "? X. X = Compl(g``Compl(f:: 'a=>'b``X))";
+goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";
 by (rtac exI 1);
 by (rtac lfp_Tarski 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));