[isabelle-dev] comparison of bindings

[Sascha Boehme]

Hi,

Given to bindings (i.e., instances of Binding.binding), how are they
supposed to be compared?

Here is a more concrete example.  Assume there is a declaration such
as:

  declare_foo name = ...

which declares "name" as some new foo-entity.  For later reference,
the declared foo-entities are best stored in a table internally,
associated with the declaration data (the omitted right-hand side
above).  Indexing this table with the binding produced from "name" is
not possible, as bindings cannot be compared with each other.  Using
Binding.print to turn a binding into a string (and using Symtab.table)
doesn't seem to be the right approach (Binding.print is probably not
meant for this purpose).  What should be used instead?

Thanks,
Sascha