--- 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 ***)