[isabelle] lift_bnf Subscript exception

The following fails in 3201ddb00097 (and most likely also Isabelle2016-RC0) with a Subscript exception:

typedef ('k, 'v) fmap = "{M :: ('k â 'v). finite (dom M)}"
  by (rule exI[of _ Map.empty]) simp_all

lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k â 'v option"]
(* exception Subscript raised (line 97 of "./basis/List.sml") *)

Can anybody tell me why? Am I doing something wrong?



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