diff -r b8a1e395edd7 -r 9f7f4fd05b1f src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Mon Apr 26 10:44:45 1999 +0200
+++ b/src/FOLP/IFOLP.thy	Mon Apr 26 13:25:49 1999 +0200
@@ -118,7 +118,7 @@
 
 whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
 whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
-plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q"
+plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
 
 applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
 funEC      "f:P ==> f = lam x. f`x : P"