# 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;