--- a/src/Pure/Thy/export_theory.ML Mon Dec 02 11:57:42 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Mon Dec 02 11:57:53 2019 +0100 @@ -67,7 +67,7 @@ |> the_default ([], false); -(* locales content *) +(* locales *) fun locale_content thy loc = let