src/ZF/AC/AC_Equiv.ML

--- a/src/ZF/AC/AC_Equiv.ML	Wed Apr 02 15:28:42 1997 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Wed Apr 02 15:29:48 1997 +0200
@@ -44,7 +44,7 @@
 
 (* used only in WO1_DC.ML *)
 (*Note simpler proof*)
-goal upair.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
+goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
 \         A<=Df; A<=Dg |] ==> f``A=g``A";
 by (asm_simp_tac (!simpset addsimps [image_fun]) 1);
 val images_eq = result();