diff -r dea357e84ac9 -r 00f3324048a7 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Wed Jan 20 10:29:25 1999 +0100
+++ b/src/HOL/ex/set.ML	Wed Jan 20 10:33:34 1999 +0100
@@ -19,12 +19,12 @@
 (** Examples for the Blast_tac paper **)
 
 (*Union-image, called Un_Union_image on equalities.ML*)
-Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
+Goal "(UN x:C. f(x) Un g(x)) = Union(f``C)  Un  Union(g``C)";
 by (Blast_tac 1);
 result();
 
 (*Inter-image, called Int_Inter_image on equalities.ML*)
-Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
+Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
 by (Blast_tac 1);
 result();