diff -r 30271d90644f -r 62b6288e6005 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Mon Jun 22 15:53:24 1998 +0200
+++ b/src/ZF/equalities.ML	Mon Jun 22 17:12:27 1998 +0200
@@ -490,12 +490,12 @@
 by (Blast_tac 1);
 qed "vimage_Int_subset";
 
-goalw thy [function_def]
+Goalw [function_def]
     "!!f. function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)";
 by (Blast_tac 1);
 qed "function_vimage_Int";
 
-goalw thy [function_def]
+Goalw [function_def]
     "!!f. function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
 by (Blast_tac 1);
 qed "function_vimage_Diff";