[isabelle] Legacy feature warning in Nitpick



Hi Jasmin,

I'm getting an odd warning when running Nitpick:

  Nitpicking formula...
  Legacy feature! Bad name binding: "â"
  Legacy feature! Bad name binding: "â"
  Nitpick found a counterexample:

  Free variables:
    t = Const sâ1
    u = Const sâ1
  Skolem constants:
    ??.matches.env = [sâ1 â Const sâ1, â â _]
    ??.matches.env = [sâ1 â Const sâ1, â â _]

I think I know what the output is trying to tell me (that there might be
other elements in the map, but we don't care), but I'm not sure where
the warning comes from. (In any case, the counterexample is correct.)

Cheers
Lars




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