# HG changeset patch # User wenzelm # Date 1004645533 -3600 # Node ID 78b8f9e133002434ad4aabc2c3e62f6590718edf # Parent 425289df84d33503713dc778acc02d18aa2a0f21 Goals.add_locale; diff -r 425289df84d3 -r 78b8f9e13300 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Thu Nov 01 21:11:52 2001 +0100 +++ b/src/Pure/Thy/thy_parse.ML Thu Nov 01 21:12:13 2001 +0100 @@ -562,7 +562,7 @@ section "local" "|> PureThy.local_path" empty_decl, section "setup" "|> Library.apply" long_id, section "MLtext" "" verbatim, - section "locale" "|> Locale.add_locale" locale_decl]; + section "locale" "|> Goals.add_locale" locale_decl]; end;