[isabelle] quotient_type command fails



Hello List,

I guess this is the right place to report bugs. If not, please refer me to the right place. Apparently in Isabelle 2013-2 the quotient_type command doesn't work, if the theory name contains white-space. In my testcase the theory was called "With Whitespace" and the command produced the following error:

attribute "Lifting.lifting_restore_internal": bad arguments
    Whitespace.foo.lifting

I attached a testcase for the problem to reproduce the issue. One theory called "WithoutWhitespace.thy", which works fine, and a copy renamed to "With Whitespace.thy", which fails.

Regards,
Salomon

theory "With Whitespace"
  imports Main
begin

quotient_type foo = "nat" / "(\<lambda>x y. True)"
  by (simp add: equivp_def)

end
theory WithoutWhitespace
  imports Main
begin

quotient_type foo = "nat" / "(\<lambda>x y. True)"
  by (simp add: equivp_def)

end


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