# HG changeset patch
# User paulson
# Date 949331608 -3600
# Node ID 988a7737e15843c2b64ea9981d8b3dc7e426e1d3
# Parent  f89329974d2df01b41876da7cb580ceb5e74b115
Pi_empty1 is a more general simprule than empty_fun

diff -r f89329974d2d -r 988a7737e158 src/ZF/func.ML
--- 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 ***)