[isabelle] Type annotations

I have two simple lemmas whose proof requires instantiating a universal
quantifier.  Could anyone tell me why the first one works and the second
one does not?  The first one can be obtained from the first one by
stripping all type annotations.  Thanks,


theory TypeSpec = Main:
typedecl obj

lemma works:
"[| ALL n1 n2. k n1 = k n2 --> n1 = n2;
     k x1 = k x2 |] ==> x1 = x2"
apply auto

lemma fails:
"[| ALL n1 n2. (k :: obj => obj) n1 = (k :: obj => obj) n2 --> n1 = n2;
     k (x1::obj) = k (x2::obj) |] ==> (x1::obj) = (x2::obj)"
apply auto


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.