src/ZF/func.ML

--- a/src/ZF/func.ML	Mon Jul 13 16:42:27 1998 +0200
+++ b/src/ZF/func.ML	Mon Jul 13 16:43:57 1998 +0200
@@ -253,7 +253,7 @@
                               addcongs [RepFun_cong]) 1);
 qed "image_fun";
 
-Goal "!!f. [| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
+Goal "[| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
 by (blast_tac (claset() addDs [apply_equality, apply_Pair]) 1);
 qed "Pi_image_cons";