[isabelle-dev] Regression in the sublocale command
ballarin at in.tum.de
Sat Feb 14 22:21:18 CET 2015
> > This might indicate that something is wrong in the local theory stack
> > here, maybe the last line in
> >> fun locale_dependency locale dep_morph mixin export =
> >> (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
> >> #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
> > from generic_target.ML
> I can confirm that.
Thanks! If you could provide me with a patch that works around the issue in the local theories, that could help me investigate the remaining problem.
The looping print_locale hints at an issue in dependency resolution itself. I don't know whether the example has ever worked (probably it has not), but I find it useful enough to pursue.
More information about the isabelle-dev