--- a/src/CTT/CTT.thy Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CTT/CTT.thy Wed Jan 12 16:33:04 2011 +0100
@@ -319,7 +319,7 @@
and "a: A"
and "!!z. z: B(a) ==> c(z): C(z)"
shows "c(p`a): C(p`a)"
-apply (rule prems ProdE)+
+apply (rule assms ProdE)+
done