src/ZF/func.thy

--- a/src/ZF/func.thy	Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/func.thy	Tue May 27 11:39:03 2003 +0200
@@ -480,7 +480,7 @@
 lemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))"
 by (unfold update_def, simp)
 
-lemma update_type: "[| f: A -> B;  x : A;  y: B |] ==> f(x:=y) : A -> B"
+lemma update_type: "[| f:Pi(A,B);  x : A;  y: B(x) |] ==> f(x:=y) : Pi(A, B)"
 apply (unfold update_def)
 apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
 done