[isabelle] updating code that calls add_locale_i



My old code included:

  Locale.add_locale_i (SOME "")
                      localename
                      (Locale.Locale globloc)
                      [e']
                      thy

What should I do now that the nearest equivalent seems to be
Expression.add_locale?  The type of the latter is a bit confusing.  In
particular, the equivalent of the (Locale.Locale globloc) looks as if
it should be a expression_i, but such expressions have to include a
term if they are to convey any useful information at all, and it's
unclear to me quite what that term should be.

Or is Expression.add_locale not the right thing to be calling?

Michael.








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