# HG changeset patch
# User lcp
# Date 788196427 -3600
# Node ID 120fc7e857ba1651810e370cf51ee2b0bb003ea6
# Parent  33dc37d4629650c453ce811db8a6016b71c0918e
empty_fun: generalized from -> to Pi

diff -r 33dc37d46296 -r 120fc7e857ba src/ZF/func.ML
--- a/src/ZF/func.ML	Fri Dec 23 16:26:34 1994 +0100
+++ b/src/ZF/func.ML	Fri Dec 23 16:27:07 1994 +0100
@@ -57,7 +57,7 @@
 qed "Pi_empty2";
 
 (*The empty function*)
-goalw ZF.thy [Pi_def, function_def] "0: 0->A";
+goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
 by (fast_tac ZF_cs 1);
 qed "empty_fun";