[isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

> > 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.

Clemens