[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
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