[isabelle] Surprisingly this verifies

The following self-contradictory theory (Two definitions contradict to each other.) verifies by Isabelle 2011. Where is the error?!

theory test
  imports HOL Main

typedecl tag

consts t1::tag
consts t2::tag

definition "f (t1, x) = t1"
definition "f (t1, x) = t2"


Victor Porton - http://portonvictor.org

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