[isabelle] [Isabelle2014-RC0] lift_definition no longer works in context with assumptions



While porting my theories to Isabelle2014-RC4, I got stuck on some lift_definition commands. In Isabelle2013-2, it was possible to issue a lift_definition command inside an unnamed context with assumptions (below is a minimal artificial example). In Isabelle2014-RC0, I do not get lift_definition to work, because it always raises the following error.

exception THM 0 raised (line 112 of "conjunction.ML"):
  dest_conjunction
  0 < ?n ⟹
  (Scratch.bar ?n = Abs_pos ?n &&& Rep_pos (Scratch.bar ?n) = ?n) &&&
  TERM TYPE(nat) &&& TERM TYPE(pos)

As the example shows, I need the assumption in lift_definition's proof obligation. How am I supposed to do this in Isabelle2014?

Best,
Andreas


theory Scratch imports "~~/src/HOL/Main" begin

typedef pos = "{n :: nat. n > 0}" by auto
setup_lifting (no_code) type_definition_pos

context
  fixes n :: nat
  assumes "n > 0"
begin

lift_definition bar :: "pos" is "n" by fact




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