--- a/src/ZF/func.ML Sun Jan 30 13:24:41 2000 +0100
+++ b/src/ZF/func.ML Mon Jan 31 16:13:28 2000 +0100
@@ -66,7 +66,7 @@
by (Blast_tac 1);
qed "singleton_fun";
-Addsimps [empty_fun, singleton_fun];
+Addsimps [Pi_empty1, singleton_fun];
(*** Function Application ***)