[isabelle] fun raises THM in context with non-function type variable

Dear Isabelle developers,

I just want to report that the function package fails with an exception THM whenever I use it in a context that fixes a variable of non-function type which is used in the function definition.

Here's a minimal example:

theory Scratch imports "~~/src/HOL/Main" begin
context fixes y :: "'a" begin
fun foo :: "unit => 'a" where "foo _ = y"

*** exception THM 0 raised (line 726 of "thm.ML"):
*** forall_intr: variable "y" free in assumptions
*** [|foo x1 = y; accp foo_rel x1;
***  !!uu_. [|x1 = uu_; y = id y; accp foo_rel uu_|] ==> P|]
*** ==> P
***   [foo == Scratch.foo y, foo_sumC == Scratch.foo_sumC y,
***     foo_graph == Scratch.foo_graph y]
*** At command "fun"

Interestingly, there's no error if I change y's type to "unit => 'a":

context fixes y :: "unit => 'a" begin
fun foo :: "unit => 'a" where "foo _ = y ()"

The same error also occurs when I change replace the unnamed context with a locale.

By the way, this is with Isabelle2013-2.


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