Goals.add_locale;
authorwenzelm
Thu, 01 Nov 2001 21:12:13 +0100 (2001-11-01)
changeset 12017 78b8f9e13300
parent 12016 425289df84d3
child 12018 ec054019c910
Goals.add_locale;
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;