src/HOL/ex/set.ML

--- a/src/HOL/ex/set.ML	Sat Oct 31 12:46:21 1998 +0100
+++ b/src/HOL/ex/set.ML	Mon Nov 02 12:35:14 1998 +0100
@@ -129,7 +129,7 @@
 by (fast_tac (claset() addEs  [inj_onD, f_eq_gE]) 1);
 qed "bij_if_then_else";
 
-Goal "!!f:: 'a=>'b.  ? X. X = - (g``(- f``X))";
+Goal "? X. X = - (g``(- (f``X)))";
 by (rtac exI 1);
 by (rtac lfp_Tarski 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));