Am 10.09.2010 um 17:26 schrieb Makarius: > So same more explanations here: > > * A local context is characterized by a mixture of Frees and Vars. The > Frees are like local constants, the Vars express generality (like > adhoc quantifiers that have already been generalized). This is > particularly important for type variables, because there is no > explicit quantification. > > * In a global situations "variables" are just "variables", they can be > either all fixed or all schematic, but not mixed. The > varify_global / unvarify_global operations allow to flip coins. The > "global" in the name indicates that something special is going on > here, outside the usual context discipline. > > It depends on the situations how things are stored in the background > context -- the typedef package prefers the free variant right now (as > does the locale infrastructure, IIRC). Digging through the history > further might explain further details, how the typedef of 9cc3df9a606e > emerged.
Thanks for the explanations. I was clearly too quick to assume this was a bug. But it remains a quirk in my eyes. Today "Typedef" is still half-local, half-global. There might come the day where it's fully localized and something like locale Foo = fixes f :: "'a => 'b" typedef bar = "UNIV::'a multiset=>bool" is accepted by Isabelle. Then the calls to "varify_global" in various tools will be broken. Assuming that full localization is the goal, wouldn't a good first step be to avoid clashes with the context in "Typedef", "Datatype", "Quotient_Type", etc.? Then tool authors could start migrating their "varify_global"s to a proper context-sensitive varify (if they haven't done so already, as I accidentally did in Nitpick). Anyway, I've already fixed Nitpick so I can live with the current situation. Jasmin _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
